From d66df2616f7523e991e779dc7896a482bb4d3482 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 29 Dec 2023 10:20:06 -0500 Subject: [PATCH] Fix some typos. (#7075) --- RELEASE_NOTES.md | 2 +- src/ast/euf/euf_ac_plugin.cpp | 6 +++--- src/ast/euf/euf_ac_plugin.h | 2 +- src/ast/euf/euf_arith_plugin.cpp | 2 +- src/ast/euf/euf_arith_plugin.h | 2 +- src/ast/euf/euf_bv_plugin.cpp | 2 +- src/muz/rel/dl_mk_similarity_compressor.cpp | 2 +- src/smt/theory_seq.cpp | 2 +- 8 files changed, 10 insertions(+), 10 deletions(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index a10af72a654..ffbe6061c0f 100644 --- a/RELEASE_NOTES.md +++ b/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 diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp index 5b4b1df664c..ce0817e009e 100644 --- a/src/ast/euf/euf_ac_plugin.cpp +++ b/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. --*/ diff --git a/src/ast/euf/euf_ac_plugin.h b/src/ast/euf/euf_ac_plugin.h index ea444b60c4d..911f539f90f 100644 --- a/src/ast/euf/euf_ac_plugin.h +++ b/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 diff --git a/src/ast/euf/euf_arith_plugin.cpp b/src/ast/euf/euf_arith_plugin.cpp index 26f8e0bd905..268eff38d81 100644 --- a/src/ast/euf/euf_arith_plugin.cpp +++ b/src/ast/euf/euf_arith_plugin.cpp @@ -7,7 +7,7 @@ Module Name: Abstract: - plugin structure for arithetic + plugin structure for arithmetic Author: diff --git a/src/ast/euf/euf_arith_plugin.h b/src/ast/euf/euf_arith_plugin.h index 7cca01f1c1a..cbdb51bef1b 100644 --- a/src/ast/euf/euf_arith_plugin.h +++ b/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 diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 89b5ade160a..6631d9e5031 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/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? diff --git a/src/muz/rel/dl_mk_similarity_compressor.cpp b/src/muz/rel/dl_mk_similarity_compressor.cpp index ea1ef42b50b..46415a0de56 100644 --- a/src/muz/rel/dl_mk_similarity_compressor.cpp +++ b/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. diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 02c0c456b9f..d27d7ba548f 100644 --- a/src/smt/theory_seq.cpp +++ b/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