diff options
Diffstat (limited to 'proofs/signatures')
| -rw-r--r-- | proofs/signatures/drat.plf | 2 | ||||
| -rw-r--r-- | proofs/signatures/lrat.plf | 12 | ||||
| -rw-r--r-- | proofs/signatures/th_lira.plf | 4 |
3 files changed, 9 insertions, 9 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 |