From 50f3e9c3c054691fefefc8b3d3f02114cd1591c8 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 6 Feb 2018 14:30:43 +0700 Subject: [PATCH] Fix typos. --- src/ast/rewriter/der.cpp | 2 +- src/duality/duality.h | 12 ++++++------ src/duality/duality_rpfp.cpp | 4 ++-- src/math/polynomial/polynomial.cpp | 10 +++++----- src/muz/spacer/spacer_unsat_core_learner.cpp | 2 +- src/qe/qe_lite.cpp | 2 +- src/smt/theory_arith_core.h | 2 +- src/smt/theory_arith_nl.h | 4 ++-- src/tactic/arith/fix_dl_var_tactic.cpp | 2 +- src/tactic/core/occf_tactic.cpp | 2 +- src/tactic/core/occf_tactic.h | 2 +- 11 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index 56f895b8a..d1fecf2fb 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -260,7 +260,7 @@ void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsig vidx = to_var(t)->get_idx(); if (fr.second == 0) { CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); - // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula. + // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula. if (definitions.get(vidx, 0) != 0) { if (visiting.is_marked(t)) { // cycle detected: remove t diff --git a/src/duality/duality.h b/src/duality/duality.h index e8f36a0cd..f1aba90bc 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -722,7 +722,7 @@ namespace Duality { check_result CheckUpdateModel(Node *root, std::vector assumps); - /** Determines the value in the counterexample of a symbol occuring in the transformer formula of + /** Determines the value in the counterexample of a symbol occurring in the transformer formula of * a given edge. */ Term Eval(Edge *e, Term t); @@ -731,7 +731,7 @@ namespace Duality { Term EvalNode(Node *p); - /** Returns true if the given node is empty in the primal solution. For proecudure summaries, + /** Returns true if the given node is empty in the primal solution. For procedure summaries, this means that the procedure is not called in the current counter-model. */ bool Empty(Node *p); @@ -854,7 +854,7 @@ namespace Duality { /** Write the RPFP to a file (currently in SMTLIB 1.2 format) */ void WriteProblemToFile(std::string filename, FileFormat format = DualityFormat); - /** Read the RPFP from a file (in specificed format) */ + /** Read the RPFP from a file (in specified format) */ void ReadProblemFromFile(std::string filename, FileFormat format = DualityFormat); /** Translate problem to Horn clause form */ @@ -870,9 +870,9 @@ namespace Duality { std::vector edges; /** Fuse a vector of transformers. If the total number of inputs of the transformers - is N, then the result is an N-ary transfomer whose output is the union of - the outputs of the given transformers. The is, suppose we have a vetor of transfoermers - {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer + is N, then the result is an N-ary transformer whose output is the union of + the outputs of the given transformers. The is, suppose we have a vector of transformers + {T_i(r_i1,...,r_iN(i) : i=1..M}. The result is a transformer F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) = T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M)) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index b6dd42f00..81ed3d017 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1491,7 +1491,7 @@ namespace Duality { return res; } - /** Determines the value in the counterexample of a symbol occuring in the transformer formula of + /** Determines the value in the counterexample of a symbol occurring in the transformer formula of * a given edge. */ RPFP::Term RPFP::Eval(Edge *e, Term t) @@ -1500,7 +1500,7 @@ namespace Duality { return dualModel.eval(tl); } - /** Returns true if the given node is empty in the primal solution. For proecudure summaries, + /** Returns true if the given node is empty in the primal solution. For proceudure summaries, this means that the procedure is not called in the current counter-model. */ bool RPFP::Empty(Node *p) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 51d8489e3..dcd5af1cc 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -1421,7 +1421,7 @@ namespace polynomial { } } - // Return the maximal variable y occuring in [m_ms + start, m_ms + end) that is smaller than x + // Return the maximal variable y occurring in [m_ms + start, m_ms + end) that is smaller than x var max_smaller_than(unsigned start, unsigned end, var x) { var max = null_var; for (unsigned i = start; i < end; i++) { @@ -1456,7 +1456,7 @@ namespace polynomial { } /** - \brief Make sure that the first monomial contains the maximal variable x occuring in the polynomial, + \brief Make sure that the first monomial contains the maximal variable x occurring in the polynomial, and x occurs with maximal degree. */ void make_first_maximal() { @@ -3209,7 +3209,7 @@ namespace polynomial { typedef sbuffer var_buffer; /** - Store in pws the variables occuring in p and their (minimal or maximal) degrees. + Store in pws the variables occurring in p and their (minimal or maximal) degrees. */ unsigned_vector m_var_degrees_tmp; template @@ -3470,7 +3470,7 @@ namespace polynomial { pp = mk_one(); return; } - // Apply filter and collect powers of x occuring in p + // Apply filter and collect powers of x occurring in p // The quick filter is the following: // If p contains a monomial x^k and no monomial of the form m*x^k m != 1, then // c = m_unit_poly @@ -3479,7 +3479,7 @@ namespace polynomial { // - found monomial x^k then iccp_powers[k]++; // - found monomial m*x^k then iccp_powers[k]+=2; // If after traversing p, there is a k s.t. iccp_powers[k] == 1, we know c == 1 - // We store iccp_powers the powers of x occuring in p. + // We store iccp_powers the powers of x occurring in p. sbuffer iccp_filter; sbuffer iccp_powers; iccp_filter.resize(d+1, 0); diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index bc066d32d..f36143c5f 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/src/muz/spacer/spacer_unsat_core_learner.cpp @@ -46,7 +46,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n"; ); - // compute symbols occuring in B + // compute symbols occurring in B collect_symbols_b(asserted_b); // traverse proof diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 3975945cb..1220bd571 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -125,7 +125,7 @@ namespace eq { vidx = to_var(t)->get_idx(); if (fr.second == 0) { CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); - // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula. + // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula. if (definitions.get(vidx, 0) != 0) { if (visiting.is_marked(t)) { // cycle detected: remove t diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index b00648c36..03830f7d0 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -40,7 +40,7 @@ namespace smt { template void theory_arith::found_underspecified_op(app * n) { if (!m_found_underspecified_op) { - TRACE("arith", tout << "found underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";); + TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, get_manager()) << "\n";); get_context().push_trail(value_trail(m_found_underspecified_op)); m_found_underspecified_op = true; } diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 87b811e8f..7eee008e9 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -141,8 +141,8 @@ namespace smt { \brief Return the number of variables that do not have bounds associated with it. The result is 0, 1, or 2. The value 2 means "2 or more". - The second value is the idx of the a variable that does not - have bounds associated with it. It is only usefull when the first value is 1. + The second value is the idx of the variable that does not + have bounds associated with it. It is only useful when the first value is 1. The second value is -1 if such variable does not exist, that is, the first value is 0. diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 7ff7bd835..2c25c12e1 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -196,7 +196,7 @@ class fix_dl_var_tactic : public tactic { app * most_occs() { // We try to choose a variable that when set to 0 will generate many bounded variables. - // That is why we give preference to variables occuring in non-nested inequalities. + // That is why we give preference to variables occurring in non-nested inequalities. unsigned best1, best2; app * r1, * r2; r1 = most_occs(m_non_nested_occs, best1); diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index 6d9d63971..254f8166c 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -9,7 +9,7 @@ Abstract: Put clauses in the assertion set in OOC (one constraint per clause) form. - Constraints occuring in formulas that + Constraints occurring in formulas that are not clauses are ignored. The formula can be put into CNF by using mk_sat_preprocessor strategy. diff --git a/src/tactic/core/occf_tactic.h b/src/tactic/core/occf_tactic.h index 80f8f6042..0ef7eb1f6 100644 --- a/src/tactic/core/occf_tactic.h +++ b/src/tactic/core/occf_tactic.h @@ -9,7 +9,7 @@ Abstract: Put clauses in the assertion set in OOC (one constraint per clause) form. - Constraints occuring in formulas that + Constraints occurring in formulas that are not clauses are ignored. The formula can be put into CNF by using mk_sat_preprocessor strategy.