diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 9cb685ccc..0271d8311 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -682,7 +682,7 @@ namespace datatype { /** \brief Return true if the inductive datatype is well-founded. - Pre-condition: The given argument constains the parameters of an inductive datatype. + Pre-condition: The given argument constrains the parameters of an inductive datatype. */ bool util::is_well_founded(unsigned num_types, sort* const* sorts) { buffer well_founded(num_types, false); diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 0bc3b43d3..3e05be734 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -154,7 +154,7 @@ namespace realclosure { struct value { unsigned m_ref_count; //!< Reference counter - bool m_rational; //!< True if the value is represented as an abitrary precision rational value. + bool m_rational; //!< True if the value is represented as an arbitrary precision rational value. mpbqi m_interval; //!< approximation as an interval with binary rational end-points // When performing an operation OP, we may have to make the width (upper - lower) of m_interval very small. // The precision (i.e., a small interval) needed for executing OP is usually unnecessary for subsequent operations, @@ -283,7 +283,7 @@ namespace realclosure { struct algebraic : public extension { polynomial m_p; mpbqi m_iso_interval; - sign_det * m_sign_det; //!< != 0 if m_iso_interval constains more than one root of m_p. + sign_det * m_sign_det; //!< != 0 if m_iso_interval constrains more than one root of m_p. unsigned m_sc_idx; //!< != UINT_MAX if m_sign_det != 0, in this case m_sc_idx < m_sign_det->m_sign_conditions.size() bool m_depends_on_infinitesimals; //!< True if the polynomial p depends on infinitesimal extensions. @@ -1741,7 +1741,7 @@ namespace realclosure { \brief In the sign determination algorithm main loop, we keep processing polynomials q, and checking whether they discriminate the roots of the target polynomial. - The vectors sc_cardinalities contains the cardinalites of the new realizable sign conditions. + The vectors sc_cardinalities contains the cardinalities of the new realizable sign conditions. That is, we started we a sequence of sign conditions sc_1, ..., sc_n, If q2_used is true, then we expanded this sequence as @@ -1750,7 +1750,7 @@ namespace realclosure { Thus, q is useful (i.e., it is a discriminator for the roots of p) IF If !q2_used, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0 - If q2_used, then There is an i s.t. AtLeatTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) + If q2_used, then There is an i s.t. AtLeastTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) */ bool keep_new_sc_assignment(unsigned sz, int const * sc_cardinalities, bool q2_used) { SASSERT(q2_used || sz % 2 == 0); @@ -2038,7 +2038,7 @@ namespace realclosure { // We should keep q only if it discriminated something. // That is, // If !use_q2, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0 - // If use_q2, then There is an i s.t. AtLeatTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) + // If use_q2, then There is an i s.t. AtLeastTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) if (!keep_new_sc_assignment(sc_cardinalities.size(), sc_cardinalities.c_ptr(), use_q2)) { // skip q since it did not reduced the cardinality of the existing sign conditions. continue; diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index ef8a9e77e..e6369a918 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -105,7 +105,7 @@ class sat_tactic : public tactic { else { // get simplified problem. #if 0 - IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";); + IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constrains interpreted atoms, recovering formula from sat solver...\"\n";); #endif m_solver.pop_to_base_level(); ref mc; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 2cf0e2651..a6b27784f 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -209,7 +209,7 @@ namespace smt { static void check_no_arithmetic(static_features const & st, char const * logic) { if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0) - throw default_exception("Benchmark constains arithmetic, but specified logic does not support it."); + throw default_exception("Benchmark constrains arithmetic, but specified logic does not support it."); } void setup::setup_QF_UF() { diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0e5393ac7..2ae445561 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -9424,15 +9424,15 @@ namespace smt { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { - int lrConstainted = 0; + int lrConstrained = 0; std::map::iterator lrit = freeVarMap.begin(); for (; lrit != freeVarMap.end(); lrit++) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { - lrConstainted = 1; + lrConstrained = 1; break; } } - if (lrConstainted == 0) { + if (lrConstrained == 0) { freeVarMap[var] = 1; } } @@ -9451,15 +9451,15 @@ namespace smt { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { - int lrConstainted = 0; + int lrConstrained = 0; std::map::iterator lrit = freeVarMap.begin(); for (; lrit != freeVarMap.end(); lrit++) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { - lrConstainted = 1; + lrConstrained = 1; break; } } - if (lrConstainted == 0) { + if (lrConstrained == 0) { freeVarMap[var] = 1; } } @@ -9471,15 +9471,15 @@ namespace smt { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { - int lrConstainted = 0; + int lrConstrained = 0; std::map::iterator lrit = freeVarMap.begin(); for (; lrit != freeVarMap.end(); lrit++) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { - lrConstainted = 1; + lrConstrained = 1; break; } } - if (lrConstainted == 0) { + if (lrConstrained == 0) { freeVarMap[var] = 1; } } @@ -9500,15 +9500,15 @@ namespace smt { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { - int lrConstainted = 0; + int lrConstrained = 0; std::map::iterator lrit = freeVarMap.begin(); for (; lrit != freeVarMap.end(); lrit++) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { - lrConstainted = 1; + lrConstrained = 1; break; } } - if (lrConstainted == 0) { + if (lrConstrained == 0) { freeVarMap[var] = 1; } } @@ -9762,7 +9762,7 @@ namespace smt { expr_ref concatlenExpr (mk_strlen(concat), m) ; bool allLeafResolved = true; if (! get_arith_value(concatlenExpr, lenValue)) { - // the length fo concat is unresolved yet + // the length of concat is unresolved yet if (get_len_value(concat, lenValue)) { // but all leaf nodes have length information TRACE("str", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;); diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 2aeb355ed..f55aa41aa 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -492,7 +492,7 @@ lbool sls_engine::search() { score = m_tracker.get_top_sum(); - // update assertion weights if a weigthing is enabled (sp < 1024) + // update assertion weights if a weighting is enabled (sp < 1024) if (m_paws) { for (unsigned i = 0; i < sz; i++) diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index 5d386862c..4bce99765 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -193,14 +193,14 @@ namespace lp { } } - void adjust_rigth_side(formula_constraint & /* c*/, lisp_elem & /*el*/) { + void adjust_right_side(formula_constraint & /* c*/, lisp_elem & /*el*/) { // lp_assert(el.m_head == "0"); // do nothing for the time being } void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) { lp_assert(el.m_elems.size() == 2); set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]); - adjust_rigth_side(c, el.m_elems[1]); + adjust_right_side(c, el.m_elems[1]); }