; 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))
((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)
(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
(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
; 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)
; 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.
;
(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
; 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
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));
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);
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;
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';
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;
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:
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;
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:
//
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());
}
/**
* 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
/**
* 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
//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;
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;
++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')
}
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;
}
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;
}
* \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.
* 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).
projects / cvc5.git / commitdiff