From: FabianWolff Date: Tue, 1 Sep 2020 03:20:57 +0000 (+0200) Subject: Fix spelling errors (#4977) X-Git-Tag: cvc5-1.0.0~2931 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa05eb5599e2ac0b2d4c1e0e943fee6353b52430;p=cvc5.git Fix spelling errors (#4977) Signed-off-by: Fabian Wolff --- diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index ad3c8ec8d..20795901f 100644 --- 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)) diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index b5d46be43..c10f8d6c8 100644 --- 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. ; diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index af326bf27..e3f6df112 100644 --- 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 diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 51ecea9f2..c14bed6aa 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3044,10 +3044,10 @@ Term Solver::mkCharFromStrHelper(const std::string& s) const 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)); @@ -5506,7 +5506,7 @@ Term Solver::getSynthSolution(Term term) const 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_node); @@ -5535,7 +5535,7 @@ std::vector Solver::getSynthSolutions( 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; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 091b5a22b..865776dcd 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2481,7 +2481,7 @@ fragment DOT:; 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'; diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index b003342c6..6641310cc 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -538,7 +538,7 @@ bool SimpSolver::eliminateVar(Var v) 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; diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 9d3a51c02..9907b8d72 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -54,7 +54,7 @@ class SimpSolver : public Solver { 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: diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index a101a0c2d..23f97b5d5 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -525,7 +525,7 @@ bool SimpSolver::eliminateVar(Var v) 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; diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 335075f09..c13ee5583 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -55,7 +55,7 @@ class SimpSolver : public Solver { 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: // diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 98e865478..955fe3e14 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -891,7 +891,7 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const 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()); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 99c4a67d3..223478e5f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -566,7 +566,7 @@ class CVC4_PUBLIC SmtEngine /** * 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 solMap that map functions-to-synthesize with diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 468535da1..621bea9f3 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -116,7 +116,7 @@ class SygusSolver /** * 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 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 9a8ca733a..7f521e2f9 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4372,7 +4372,7 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound //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; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index dd59628c1..cb7a4d055 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -575,7 +575,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ 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; diff --git a/src/util/string.cpp b/src/util/string.cpp index 44c4d3e4b..a1a40df8a 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -131,7 +131,7 @@ std::vector String::toInternal(const std::string& s, ++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 @@ std::vector String::toInternal(const std::string& s, } 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 @@ std::vector String::toInternal(const std::string& s, 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; } diff --git a/src/util/string.h b/src/util/string.h index ca458232f..fb4a1208c 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -58,7 +58,7 @@ class CVC4_PUBLIC String { * \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. @@ -213,7 +213,7 @@ class CVC4_PUBLIC String { * 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).