Typo fixes.

Author: waywardmonkeys

README-CMake.md

@@ -5,7 +5,7 @@ of the project written in the ``CMakeLists.txt`` files and emits a build
 system for that project of your choice using one of CMake's "generators".
 This allows CMake to support many different platforms and build tools.
 You can run ``cmake --help`` to see the list of supported "generators"
-on your platform. Example generators include "UNIX Makfiles" and "Visual Studio
+on your platform. Example generators include "UNIX Makefiles" and "Visual Studio
 12 2013".
 
 ## Getting started
@@ -44,7 +44,7 @@ cmake -G "Unix Makefiles" ../
 make -j4 # Replace 4 with an appropriate number
 ```
 
-Note that on some platforms "Unix Makesfiles" is the default generator so on those
+Note that on some platforms "Unix Makefiles" is the default generator so on those
 platforms you don't need to pass ``-G "Unix Makefiles"`` command line option to
 ``cmake``.
 

RELEASE_NOTES

@@ -712,7 +712,7 @@ The following bugs are fixed in this release:
   bvshl when using a shift amount that evaluates to the length
   of the bit-vector. Thanks to Trevor Hansen and Robert Brummayer. 
 
-- Incorrect NNF conversion in linear quantifier elimniation routines.
+- Incorrect NNF conversion in linear quantifier elimination routines.
   Thanks to Josh Berdine.
 
 - Missing constant folding of extraction for large bit-vectors.

cmake/Z3Config.cmake.in

@@ -2,7 +2,7 @@
 # @AUTO_GEN_MSG@
 #
 # This file is intended to be consumed by clients who wish to use Z3 from CMake.
-# It can be use by doing `find_package(Z3 config)` from within a
+# It can be used by doing `find_package(Z3 config)` from within a
 # `CMakeLists.txt` file. If CMake doesn't find this package automatically you
 # can give it a hint by passing `-DZ3_DIR=<path>` to the CMake invocation where
 # `<path>` is the path to the directory containing this file.

contrib/suppressions/sanitizers/README.md

@@ -1,4 +1,4 @@
-# Sanitizer supression files
+# Sanitizer suppression files
 
 This directory contains files used to suppress
 ASan/LSan/UBSan warnings/errors.

examples/c/test_capi.c

@@ -1546,7 +1546,7 @@ void two_contexts_example1()
 }
 
 /**
-   \brief Demonstrates how error codes can be read insted of registering an error handler.
+   \brief Demonstrates how error codes can be read instead of registering an error handler.
  */
 void error_code_example1()
 {
@@ -2533,7 +2533,7 @@ void reference_counter_example() {
 
     cfg                = Z3_mk_config();
     Z3_set_param_value(cfg, "model", "true");
-    // Create a Z3 context where the user is reponsible for managing
+    // Create a Z3 context where the user is responsible for managing
     // Z3_ast reference counters.
     ctx                = Z3_mk_context_rc(cfg);
     Z3_del_config(cfg);

examples/dotnet/Program.cs

@@ -622,7 +622,7 @@ static void QuantifierExample2(Context ctx)
                 Console.WriteLine("{0}", q1);
             }
 
-            // Quantifier with de-Brujin indices.
+            // Quantifier with de-Bruijn indices.
             {
                 Expr x = ctx.MkBound(1, ctx.IntSort);
                 Expr y = ctx.MkBound(0, ctx.IntSort);

examples/java/JavaExample.java

@@ -660,7 +660,7 @@ void quantifierExample2(Context ctx)
             System.out.println(q1);
         }
 
-        // Quantifier with de-Brujin indices.
+        // Quantifier with de-Bruijn indices.
         {
             Expr x = ctx.mkBound(1, ctx.getIntSort());
             Expr y = ctx.mkBound(0, ctx.getIntSort());

examples/maxsat/README

@@ -9,4 +9,4 @@ On OSX and Linux, you must install z3 first using
    sudo make install
 OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library.
 
-This directory contains a test file (ex.smt) that can be use as input for the maxsat test application.
+This directory contains a test file (ex.smt) that can be used as input for the maxsat test application.

src/api/dotnet/Context.cs

@@ -2262,7 +2262,7 @@ public ArrayExpr MkConstArray(Sort domain, Expr v)
         /// Maps f on the argument arrays.
         /// </summary>
         /// <remarks>
-        /// Eeach element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
+        /// Each element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
         /// The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
         /// <c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
         /// <seealso cref="MkArraySort(Sort, Sort)"/>
@@ -2862,7 +2862,7 @@ public Expr MkNumeral(string v, Sort ty)
         }
 
         /// <summary>
-        /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
+        /// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
         /// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
         /// </summary>
         /// <param name="v">Value of the numeral</param>
@@ -2878,7 +2878,7 @@ public Expr MkNumeral(int v, Sort ty)
         }
 
         /// <summary>
-        /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
+        /// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
         /// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
         /// </summary>
         /// <param name="v">Value of the numeral</param>
@@ -2894,7 +2894,7 @@ public Expr MkNumeral(uint v, Sort ty)
         }
 
         /// <summary>
-        /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
+        /// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
         /// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
         /// </summary>
         /// <param name="v">Value of the numeral</param>
@@ -2910,7 +2910,7 @@ public Expr MkNumeral(long v, Sort ty)
         }
 
         /// <summary>
-        /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
+        /// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
         /// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
         /// </summary>
         /// <param name="v">Value of the numeral</param>
@@ -3211,7 +3211,7 @@ public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pa
         /// Create an existential Quantifier.
         /// </summary>
         /// <remarks>
-        /// Creates an existential quantifier using de-Brujin indexed variables.
+        /// Creates an existential quantifier using de-Bruijn indexed variables.
         /// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
         /// </remarks>
         public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)

src/api/dotnet/Expr.cs

@@ -959,7 +959,7 @@ public bool IsBV
         /// Tn: (R t_n s_n)
         /// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
         /// Remark: if t_i == s_i, then the antecedent Ti is suppressed.
-        /// That is, reflexivity proofs are supressed to save space.
+        /// That is, reflexivity proofs are suppressed to save space.
         /// </remarks>
         public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
 
@@ -1002,7 +1002,7 @@ public bool IsBV
         public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
 
         /// <summary>
-        /// Indicates whether the term is a proof by eliminiation of not-or
+        /// Indicates whether the term is a proof by elimination of not-or
         /// </summary>
         /// <remarks>
         /// Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
@@ -1112,7 +1112,7 @@ public bool IsBV
         public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
 
         /// <summary>
-        /// Indicates whether the term is a hypthesis marker.
+        /// Indicates whether the term is a hypothesis marker.
         /// </summary>
         /// <remarks>Mark a hypothesis in a natural deduction style proof.</remarks>
         public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
@@ -1433,7 +1433,7 @@ public bool IsRelation
         /// <remarks>
         /// Filter (restrict) a relation with respect to a predicate.
         /// The first argument is a relation.
-        /// The second argument is a predicate with free de-Brujin indices
+        /// The second argument is a predicate with free de-Bruijn indices
         /// corresponding to the columns of the relation.
         /// So the first column in the relation has index 0.
         /// </remarks>
@@ -1649,7 +1649,7 @@ public bool IsFPRMExpr {
         public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
 
         /// <summary>
-        /// Indicates whether the term is a floating-point divison term
+        /// Indicates whether the term is a floating-point division term
         /// </summary>
         public bool IsFPDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }
 
@@ -1709,7 +1709,7 @@ public bool IsFPRMExpr {
         public bool IsFPLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }
 
         /// <summary>
-        /// Indicates whether the term is a floating-point greater-than or erqual term
+        /// Indicates whether the term is a floating-point greater-than or equal term
         /// </summary>
         public bool IsFPGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }
 
@@ -1789,7 +1789,7 @@ public bool IsFPRMExpr {
 
         #region Bound Variables
         /// <summary>
-        /// The de-Burijn index of a bound variable.
+        /// The de-Bruijn index of a bound variable.
         /// </summary>
         /// <remarks>
         /// Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain

src/api/dotnet/Model.cs

@@ -253,7 +253,7 @@ public Expr Evaluate(Expr t, bool completion = false)
         /// The uninterpreted sorts that the model has an interpretation for. 
         /// </summary>
         /// <remarks>
-        /// Z3 also provides an intepretation for uninterpreted sorts used in a formula.
+        /// Z3 also provides an interpretation for uninterpreted sorts used in a formula.
         /// The interpretation for a sort is a finite set of distinct values. We say this finite set is
         /// the "universe" of the sort.
         /// </remarks>

src/api/java/Context.java

@@ -2234,7 +2234,7 @@ public Expr mkNumeral(String v, Sort ty)
     }
 
     /**
-     * Create a Term of a given sort. This function can be use to create
+     * Create a Term of a given sort. This function can be used to create
      * numerals that fit in a machine integer. It is slightly faster than
      * {@code MakeNumeral} since it is not necessary to parse a string.
      * 
@@ -2250,7 +2250,7 @@ public Expr mkNumeral(int v, Sort ty)
     }
 
     /**
-     * Create a Term of a given sort. This function can be use to create
+     * Create a Term of a given sort. This function can be used to create
      * numerals that fit in a machine integer. It is slightly faster than
      * {@code MakeNumeral} since it is not necessary to parse a string.
      * 
@@ -2438,7 +2438,7 @@ public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
     }
 
     /**
-     * Creates an existential quantifier using de-Brujin indexed variables. 
+     * Creates an existential quantifier using de-Bruijn indexed variables.
      * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,

src/api/java/Expr.java

@@ -1421,7 +1421,7 @@ public boolean isProofTransitivityStar()
      * Remarks:  T1:
      * (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ...
      * t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is
-     * suppressed. That is, reflexivity proofs are supressed to save space.
+     * suppressed. That is, reflexivity proofs are suppressed to save space.
      * 
      * @throws Z3Exception on error
      * @return a boolean
@@ -1473,7 +1473,7 @@ public boolean isProofAndElimination()
     }
 
     /**
-     * Indicates whether the term is a proof by eliminiation of not-or 
+     * Indicates whether the term is a proof by elimination of not-or
      * Remarks:  * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i) 
      * @throws Z3Exception on error
      * @return a boolean
@@ -1605,7 +1605,7 @@ public boolean isProofQuantInst()
     }
 
     /**
-     * Indicates whether the term is a hypthesis marker.
+     * Indicates whether the term is a hypothesis marker.
      * Remarks: Mark a
      * hypothesis in a natural deduction style proof.
      * @throws Z3Exception on error
@@ -1987,7 +1987,7 @@ public boolean isRelationProject()
      * Indicates whether the term is a relation filter
      * Remarks:  Filter
      * (restrict) a relation with respect to a predicate. The first argument is
-     * a relation. The second argument is a predicate with free de-Brujin
+     * a relation. The second argument is a predicate with free de-Bruijn
      * indices corresponding to the columns of the relation. So the first column
      * in the relation has index 0. 
      * @throws Z3Exception on error
@@ -2094,7 +2094,7 @@ public boolean isFiniteDomainLT()
     }
 
     /**
-     * The de-Burijn index of a bound variable.
+     * The de-Bruijn index of a bound variable.
      * Remarks:  Bound variables are
      * indexed by de-Bruijn indices. It is perhaps easiest to explain the
      * meaning of de-Bruijn indices by indicating the compilation process from

src/api/java/Model.java

@@ -239,7 +239,7 @@ public int getNumSorts()
 
     /**
      * The uninterpreted sorts that the model has an interpretation for.
-     * Remarks:  Z3 also provides an intepretation for uninterpreted sorts used
+     * Remarks:  Z3 also provides an interpretation for uninterpreted sorts used
      * in a formula. The interpretation for a sort is a finite set of distinct
      * values. We say this finite set is the "universe" of the sort. 
      *