diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 8 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 2 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 2 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 | ||||
-rw-r--r-- | src/smt/sygus_solver.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 | ||||
-rw-r--r-- | src/util/string.cpp | 6 | ||||
-rw-r--r-- | src/util/string.h | 4 |
13 files changed, 19 insertions, 19 deletions
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<uint32_t>(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<unsigned> cpts; cpts.push_back(val); return mkValHelper<CVC4::String>(CVC4::String(cpts)); @@ -5506,7 +5506,7 @@ Term Solver::getSynthSolution(Term term) const std::map<CVC4::Node, CVC4::Node> 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<CVC4::Node, CVC4::Node>::const_iterator it = map.find(*term.d_node); @@ -5535,7 +5535,7 @@ std::vector<Term> Solver::getSynthSolutions( std::map<CVC4::Node, CVC4::Node> 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<Term> 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<Lit>& 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<Lit>& 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<unsigned> 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<unsigned> 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<unsigned> 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). |