Fix some typos. (#7075)

Author: waywardmonkeys

RELEASE_NOTES.md

@@ -16,7 +16,7 @@ Version 4.12.5
 - A new theory solver "int-blast" enabled by using:
   - sat.smt=true smt.bv.solver=2
   - It solves a few bit-vector problems not handled by bit-blasting, especially if the bit-widths are large.
-  - It is based on encoding bit-vector constraints to non-linear integer arithemtic.
+  - It is based on encoding bit-vector constraints to non-linear integer arithmetic.
 
 
 Version 4.12.4

src/ast/euf/euf_ac_plugin.cpp

@@ -59,9 +59,9 @@ More notes:
   - The shared terms hash table is not incremental. 
     It could be made incremental by updating it on every merge similar to how the egraph handles it.
 - V2 using multiplicities instead of repeated values in monomials.
-- Squash trail updates when equations or monomials are modified within the same epoque. 
-  - by an epoque counter that can be updated by the egraph class whenever there is a push/pop.
-  - store the epoque as a tick on equations and possibly when updating monomials on equations.
+- Squash trail updates when equations or monomials are modified within the same epoch.
+  - by an epoch counter that can be updated by the egraph class whenever there is a push/pop.
+  - store the epoch as a tick on equations and possibly when updating monomials on equations.
 
 --*/
 

src/ast/euf/euf_ac_plugin.h

@@ -40,7 +40,7 @@ namespace euf {
         struct node {
             enode* n;        // associated enode
             node* root;      // path compressed root
-            node* next;      // next in equaivalence class
+            node* next;      // next in equivalence class
             justification j; // justification for equality
             node* target = nullptr;    // justified next
             unsigned_vector shared;    // shared occurrences

src/ast/euf/euf_arith_plugin.cpp

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    plugin structure for arithetic
+    plugin structure for arithmetic
 
 Author:
 

src/ast/euf/euf_arith_plugin.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    plugin structure for arithetic
+    plugin structure for arithmetic
 Author:
 
     Nikolaj Bjorner (nbjorner) 2023-11-11

src/ast/euf/euf_bv_plugin.cpp

@@ -69,7 +69,7 @@ The formal properties of saturation have to be established.
 - Saturation does not complete with respect to associativity.
 Instead the claim is along the lines that the resulting E-graph can be used as a canonizer.
 If given a set of equations E that are saturated, and terms t1, t2 that are 
-both simplified with respect to left-associativity of concatentation, and t1, t2 belong to the E-graph,
+both simplified with respect to left-associativity of concatenation, and t1, t2 belong to the E-graph,
 then t1 = t2 iff t1 ~ t2 in the E-graph.
 
 TODO: Is saturation for (7) overkill for the purpose of canonization?

src/muz/rel/dl_mk_similarity_compressor.cpp

@@ -101,7 +101,7 @@ namespace datalog {
 
     /**
        \brief Return 0 if r1 and r2 could be similar. If the rough similarity
-       equaivelance class of r1 is greater than the one of r2, return 1; otherwise return -1.
+       equivalence class of r1 is greater than the one of r2, return 1; otherwise return -1.
 
        Two rules are in the same rough similarity class if they differ only in constant arguments
        of positive uninterpreted predicates.

src/smt/theory_seq.cpp

@@ -1244,7 +1244,7 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
 
 /**
  * solve for fold/map (recursive function that depends on a sequence)
- * Assumption: the Seq argument of fold/map expands into a concatentation of units
+ * Assumption: the Seq argument of fold/map expands into a concatenation of units
  * The assumption is enforced by tracking the length of the seq argument.
  * This is ensured in relevant_eh.
  * Under the assumption, evern occurrence of fold/map gets simplified by expanding