From 1d9345c3debdc7705cac43717db0a0c3a1c808f1 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sun, 31 Jul 2022 12:44:26 +0700 Subject: [PATCH] Fix typos. --- src/ast/seq_decl_plugin.h | 2 +- src/math/grobner/pdd_simplifier.cpp | 4 ++-- src/math/lp/emonics.cpp | 2 +- src/math/lp/mps_reader.h | 2 +- src/model/datatype_factory.cpp | 2 +- src/muz/base/dl_context.h | 2 +- src/muz/rel/aig_exporter.cpp | 2 +- src/muz/rel/dl_base.h | 4 ++-- src/muz/rel/dl_relation_manager.cpp | 4 ++-- src/opt/maxcore.cpp | 8 ++++---- src/smt/theory_pb.cpp | 2 +- src/test/lp/smt_reader.h | 2 +- src/util/cmd_context_types.h | 2 +- 13 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index d5c6da187..30b4a9fb3 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -448,7 +448,7 @@ public: info() {} /* - Used for constructing either an invalid info that is only used to indicate uninitialzed entry, or valid but unknown info value. + Used for constructing either an invalid info that is only used to indicate uninitialized entry, or valid but unknown info value. */ info(lbool is_known) : known(is_known) {} diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp index e8b10ad80..4a8140681 100644 --- a/src/math/grobner/pdd_simplifier.cpp +++ b/src/math/grobner/pdd_simplifier.cpp @@ -19,7 +19,7 @@ Extended Linear Simplification (as exploited in Bosphorus AAAI 2019): - multiply each polynomial by one variable from their orbits. - - The orbit of a varible are the variables that occur in the same monomial as it in some polynomial. + - The orbit of a variable are the variables that occur in the same monomial as it in some polynomial. - The extended set of polynomials is fed to a linear Gauss Jordan Eliminator that extracts additional linear equalities. - Bosphorus uses M4RI to perform efficient GJE to scale on large bit-matrices. @@ -32,7 +32,7 @@ The method seems rather specific to hardware multipliers so not clear it is useful to generalize. - find monomials that contain pairs of vanishing polynomials, transitively - withtout actually inlining. + without actually inlining. Then color polynomial variables w by p, resp, q if they occur in polynomial equalities w - r = 0, such that all paths in r contain a node colored by p, resp q. polynomial variables that get colored by both p and q can be set to 0. diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index 5b3ae64f0..0f1956a2b 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -518,7 +518,7 @@ std::ostream& emonics::display(std::ostream& out, cell* c) const { bool emonics::invariant() const { TRACE("nla_solver_mons", display(tout);); - // the varible index contains exactly the active monomials + // the variable index contains exactly the active monomials unsigned mons = 0; for (lpvar v = 0; v < m_var2index.size(); v++) { if (is_monic_var(v)) { diff --git a/src/math/lp/mps_reader.h b/src/math/lp/mps_reader.h index f0fa074cc..f2cf2d320 100644 --- a/src/math/lp/mps_reader.h +++ b/src/math/lp/mps_reader.h @@ -20,7 +20,7 @@ Revision History: #pragma once -// reads an MPS file reperesenting a Mixed Integer Program +// reads an MPS file representing a Mixed Integer Program #include #include #include diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index 56312839a..c01b385d7 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -87,7 +87,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) { return val; } // Traverse constructors, and try to invoke get_fresh_value of one of the arguments (if the argument is not a sibling datatype of s). - // If the argumet is a sibling datatype of s, then + // If the argument is a sibling datatype of s, then // use get_last_fresh_value. ptr_vector const & constructors = *m_util.get_datatype_constructors(s); for (func_decl * constructor : constructors) { diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index e9ee4c690..eae846835 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -305,7 +305,7 @@ namespace datalog { void register_predicate(func_decl * pred, bool named); /** - Restrict reltaions to set of predicates. + Restrict relations to set of predicates. */ void restrict_predicates(func_decl_set const& preds); diff --git a/src/muz/rel/aig_exporter.cpp b/src/muz/rel/aig_exporter.cpp index c8ef1321f..e708c1457 100644 --- a/src/muz/rel/aig_exporter.cpp +++ b/src/muz/rel/aig_exporter.cpp @@ -35,7 +35,7 @@ namespace datalog { // reserve pred id = 0 for initialization purposes unsigned num_preds = (unsigned)predicates.size() + 1; - // poor's man round-up log2 + // poor man's round-up log2 unsigned preds_bitsize = log2(num_preds); if ((1U << preds_bitsize) < num_preds) ++preds_bitsize; diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 1a4125ed4..376b41d34 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -73,7 +73,7 @@ namespace datalog { /** - Termplate class containing common infrastructure for relations and tables + Template class containing common infrastructure for relations and tables */ template struct tr_infrastructure { @@ -881,7 +881,7 @@ namespace datalog { public: virtual ~table_row_pair_reduce_fn() {} /** - \brief The function is called for pair of table rows that became duplicit due to projection. + \brief The function is called for pair of table rows that became duplicated due to projection. The values that are in the first array after return from the function will be used for the resulting row. diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 51e7f4ac6..a782cc143 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1230,11 +1230,11 @@ namespace datalog { /** - An auixiliary class for functors that perform filtering. It performs the table traversal + An auxiliary class for functors that perform filtering. It performs the table traversal and only asks for each individual row whether it should be removed. When using this class in multiple inheritance, this class should not be inherited publicly - and should be mentioned as last. This should ensure that deteletion of the object will + and should be mentioned as last. This should ensure that deletion of the object will go well when initiated from a pointer to the first ancestor. */ class relation_manager::auxiliary_table_filter_fn { diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp index 1789f0675..d29da86f7 100644 --- a/src/opt/maxcore.cpp +++ b/src/opt/maxcore.cpp @@ -12,8 +12,8 @@ Abstract: - mu: max-sat algorithm by Nina and Bacchus, AAAI 2014. - mus-mss: based on dual refinement of bounds. - binary: binary version of maxres - - rc2: implementaion of rc2 heuristic using cardinality constraints - - rc2t: implementaion of rc2 heuristic using totalizerx + - rc2: implementation of rc2 heuristic using cardinality constraints + - rc2t: implementation of rc2 heuristic using totalizerx - rc2-binary: hybrid of rc2 and binary maxres. Perform one step of binary maxres. If there are more than 16 soft constraints create a cardinality constraint. @@ -27,7 +27,7 @@ Abstract: constraints the approach works like max-res. Given a (maximal) satisfying subset of the soft constraints the approach updates the upper bound if the current assignment - improves the current best assignmet. + improves the current best assignment. Furthermore, take the soft constraints that are complements to the current satisfying subset. E.g, if F are the hard constraints and @@ -44,7 +44,7 @@ Abstract: If k of these soft clauses are false in the satisfying assignment for the updated F, then k of the original soft clauses are also false under the assignment. - In summary: any assignment to the new clauses that satsfies F has the + In summary: any assignment to the new clauses that satisfies F has the same cost. Claim: If there are no satisfying assignments to F, then the current best assignment diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index f24e4746d..8809030e3 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1106,7 +1106,7 @@ namespace smt { \brief propagate assignment to inequality. This is a basic, non-optimized implementation based on the assumption that inequalities are mostly units - and/or relatively few compared to number of argumets. + and/or relatively few compared to number of arguments. */ void theory_pb::assign_ineq(ineq& c, bool is_true) { m_mpz_trail.push_back(c.m_max_sum); diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index e641410db..2ab0c1ea6 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -20,7 +20,7 @@ Revision History: #pragma once -// reads an MPS file reperesenting a Mixed Integer Program +// reads an MPS file representing a Mixed Integer Program #include #include #include diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h index 80e284d90..5195333fc 100644 --- a/src/util/cmd_context_types.h +++ b/src/util/cmd_context_types.h @@ -78,7 +78,7 @@ typedef std::pair sorted_var; /** \brief Command abstract class. - Commands may have variable number of argumets. + Commands may have variable number of arguments. */ class cmd { symbol m_name;