Description: Fix spelling errors found by Lintian Author: Fabian Wolff Forwarded: https://github.com/CVC4/CVC4/pull/4977 Last-Update: 2020-08-31 --- This patch header follows DEP-3: http://dep.debian.net/deps/dep3/ --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -354,7 +354,7 @@ ; Helper for `is_operational_drat_proof` which takes a UP model for the working ; formula. The UP model is important for determining which clause deletions ; actually are executed in operational DRAT. Passing the UP model along -; prevents it from being fully recomputed everytime. +; prevents it from being fully recomputed every time. (program is_operational_drat_proof_h ((f cnf) (up_model clause) (pf DRATProof)) bool (match pf (DRATProofn (cnf_has_bottom f)) --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -101,7 +101,7 @@ ((pos v2) ff) ((neg v2) (ifequal v1 v2 tt ff)))))) -; Remove **all** occurences of a literal from clause +; Remove **all** occurrences of a literal from clause (program clause_remove_all ((l lit) (c clause)) clause (match c (cln cln) @@ -180,7 +180,7 @@ (CMapc ci c (CMap_remove_many is cs')))))))) ; Given a map of clauses and a literal, return all indices in the map -; corresponsing to clauses that could resolve against that literal. i.e. for x, +; corresponding to clauses that could resolve against that literal. i.e. for x, ; return the indices of all clauses containing x. (program collect_resolution_targets_w_lit ((cs CMap) (l lit)) CIList (match cs @@ -260,14 +260,14 @@ (fail Unit) (ifmarked2 v unit (do (markvar2 v) unit)))))) -; Unmarks the variable within a satified literal to render it neither satified nor falsified +; Unmarks the variable within a satisfied literal to render it neither satisfied nor falsified ; fails if the literal is not already satisfied (program lit_un_mk_sat ((l lit)) Unit (match l ((pos v) (ifmarked1 v (do (markvar1 v) unit) (fail Unit))) ((neg v) (ifmarked2 v (do (markvar2 v) unit) (fail Unit))))) -; Unmarks the variable within a falsified literal to render it neither satified nor falsified +; Unmarks the variable within a falsified literal to render it neither satisfied nor falsified ; fails if the literal is not already falsified (program lit_un_mk_unsat ((l lit)) Unit (match l @@ -348,7 +348,7 @@ ; The return type for verifying that a clause is unit and modifying the global ; assignment to satisfy it (declare MarkResult type) -; The clause is unit, and this is the (previoiusly floating) literal that is now satified. +; The clause is unit, and this is the (previoiusly floating) literal that is now satisfied. (declare MRUnit (! l lit MarkResult)) ; The clause was unsat! (declare MRUnsat MarkResult) @@ -357,7 +357,7 @@ ; The clause had multiple floating literals. (declare MRNotUnit MarkResult) -; Determine wether this clause is sat, unsat, unit, or not unit, and if it is +; Determine whether this clause is sat, unsat, unit, or not unit, and if it is ; unit, it modifies the global assignment to satisfy the clause, and returns ; the literal that was made SAT by the new mark. ; --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2684,10 +2684,10 @@ CVC4_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0) == std::string::npos && s.size() <= 5 && s.size() > 0) - << "Unexpected string for hexidecimal character " << s; + << "Unexpected string for hexadecimal character " << s; uint32_t val = static_cast(std::stoul(s, 0, 16)); CVC4_API_CHECK(val < String::num_codes()) - << "Not a valid code point for hexidecimal character " << s; + << "Not a valid code point for hexadecimal character " << s; std::vector cpts; cpts.push_back(val); return mkValHelper(CVC4::String(cpts)); @@ -5042,7 +5042,7 @@ std::map map; CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) - << "The solver is not in a state immediately preceeded by a " + << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; std::map::const_iterator it = map.find(*term.d_expr); @@ -5071,7 +5071,7 @@ std::map map; CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) - << "The solver is not in a state immediately preceeded by a " + << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; std::vector synthSolution; --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2488,7 +2488,7 @@ fragment DOTDOT:; /** - * Matches the hexidecimal digits (0-9, a-f, A-F) + * Matches the hexadecimal digits (0-9, a-f, A-F) */ fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4763,7 +4763,7 @@ //We are only going to recreate the functionality for now. //In the future this can be improved to generate a temporary constraint //if none exists. - //Experiment with doing this everytime or only when the new constraint + //Experiment with doing this every time or only when the new constraint //implies an unknown fact. ConstraintType t = upperBound ? UpperBound : LowerBound; --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -131,7 +131,7 @@ ++i; // are we an escape sequence? bool isEscapeSequence = true; - // the string corresponding to the hexidecimal code point + // the string corresponding to the hexadecimal code point std::stringstream hexString; // is the slash followed by a 'u'? Could be last character. if (i >= s.size() || s[i] != 'u') @@ -195,7 +195,7 @@ } if (!isEnd) { - // if we were interupted before ending, then this is not a valid + // if we were interrupted before ending, then this is not a valid // escape sequence isEscapeSequence = false; } @@ -210,7 +210,7 @@ if (val > num_codes()) { // Failed due to being out of range. This can happen for strings of - // the form \ u { d_4 d_3 d_2 d_1 d_0 } where d_4 is a hexidecimal not + // the form \ u { d_4 d_3 d_2 d_1 d_0 } where d_4 is a hexadecimal not // in the range [0-2]. isEscapeSequence = false; } --- a/src/util/string.h +++ b/src/util/string.h @@ -58,7 +58,7 @@ * \u{d_2 d_1 d_0} * \u{d_3 d_2 d_1 d_0} * \u{d_4 d_3 d_2 d_1 d_0} - * where d_0 ... d_4 are hexidecimal digits, to the appropriate character. + * where d_0 ... d_4 are hexadecimal digits, to the appropriate character. * * If useEscSequences is false, then the characters of the constructed * CVC4::String correspond one-to-one with the input string. @@ -211,7 +211,7 @@ * This is true for code points between 48 ('0') and 57 ('9'). */ static bool isDigit(unsigned character); - /** is the unsigned a hexidecimal digit? + /** is the unsigned a hexadecimal digit? * * This is true for code points between 48 ('0') and 57 ('9'), code points * between 65 ('A') and 70 ('F) and code points between 97 ('a') and 102 ('f). --- a/proofs/signatures/th_lira.plf +++ b/proofs/signatures/th_lira.plf @@ -128,7 +128,7 @@ (default (fail (term Int))) )) -; This function negates linear interger terms---sums of terms of the form +; This function negates linear integer terms---sums of terms of the form ; recognized by `negate_linear_monomial_int_term`. (program negate_linear_int_term ((t (term Int))) (term Int) (match t @@ -339,7 +339,7 @@ ; the statement that `a` satisfies `b` for all inputs (declare bounded_aff (! a aff (! b bound formula))) -; Sum of two bounds (the bound satisfied by the sum of two functions satifying +; Sum of two bounds (the bound satisfied by the sum of two functions satisfying ; the input bounds) (program bound_add ((b bound) (b2 bound)) bound (match b --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1450,7 +1450,7 @@ std::stringstream ss; ss << "Cannot " << c << " since model is not available. Perhaps the most recent call to " - "check-sat was interupted?"; + "check-sat was interrupted?"; throw RecoverableModalException(ss.str().c_str()); } --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -582,7 +582,7 @@ Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl; if( needsCheck ){ - //flush previous lemmas (for instance, if was interupted), or other lemmas to process + //flush previous lemmas (for instance, if was interrupted), or other lemmas to process flushLemmas(); if( d_hasAddedLemma ){ return; --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -54,7 +54,7 @@ Lit r, ClauseId& id); // Add a ternary clause to the solver. bool addClause_(vec& ps, ClauseId& id); - bool substitute(Var v, Lit x); // Replace all occurences of v with x (may + bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may // cause a contradiction). // Variable mode: --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -55,7 +55,7 @@ bool addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver. bool addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver. bool addClause_(vec& ps, bool removable, ClauseId& id); - bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). + bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may cause a contradiction). // Variable mode: // --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -562,7 +562,7 @@ /** * Get synth solution. * - * This method returns true if we are in a state immediately preceeded by + * This method returns true if we are in a state immediately preceded by * a successful call to checkSynth. * * This method adds entries to sol_map that map functions-to-synthesize with --- a/src/theory/example/ecdata.h +++ b/src/theory/example/ecdata.h @@ -165,7 +165,7 @@ * Pointer to the end of the watch-list. * This is maintained in order to constant time list merging. * (This does not give any asymptotic improve as this is currently always - * preceeded by an O(|watchlist|) operation.) + * preceded by an O(|watchlist|) operation.) * This value is NULL iff the watch list is empty. */ Link* d_last; --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -538,7 +538,7 @@ for (int i = 0; i < cls.size(); i++) (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]); - // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no + // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no // clause must exceed the limit on the maximal clause size (if it is set): // int cnt = 0; --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -525,7 +525,7 @@ for (int i = 0; i < cls.size(); i++) (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]); - // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no + // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no // clause must exceed the limit on the maximal clause size (if it is set): // int cnt = 0; --- a/src/theory/example/theory_uf_tim.h +++ b/src/theory/example/theory_uf_tim.h @@ -163,7 +163,7 @@ bool equiv(TNode x, TNode y); /** - * Merges 2 equivalence classes, checks wether any predecessors need to + * Merges 2 equivalence classes, checks whether any predecessors need to * be set equal to complete congruence closure. * The class with the smaller class size will be merged. * @pre ecX->isClassRep()