summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/signatures/drat.plf2
-rw-r--r--proofs/signatures/lrat.plf12
-rw-r--r--proofs/signatures/th_lira.plf4
-rw-r--r--src/api/cvc4cpp.cpp8
-rw-r--r--src/parser/cvc/Cvc.g2
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.cc2
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.h2
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc2
-rw-r--r--src/prop/minisat/simp/SimpSolver.h2
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/smt/smt_engine.h2
-rw-r--r--src/smt/sygus_solver.h2
-rw-r--r--src/theory/arith/theory_arith_private.cpp2
-rw-r--r--src/theory/quantifiers_engine.cpp2
-rw-r--r--src/util/string.cpp6
-rw-r--r--src/util/string.h4
16 files changed, 28 insertions, 28 deletions
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<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).
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback