add some comments

potassco · Dec 5, 2024 · 4a37f10 · 4a37f10
1 parent c3dbe01
commit 4a37f10
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/src/translating/ordered_completion.rs b/src/translating/ordered_completion.rs
@@ -59,15 +59,18 @@ pub fn ordered_completion(theory: fol::Theory) -> Option<fol::Theory> {
 }
 
 fn create_order_formula(p: fol::Atom, q: fol::Atom) -> fol::Formula {
+    // creates the atomic formula less_p_q(xs, ys)
+    // where p(xs) and q(ys) are the given atoms
     fol::Formula::AtomicFormula(fol::AtomicFormula::Atom(fol::Atom {
         predicate_symbol: format!("less_{}_{}", p.predicate_symbol, q.predicate_symbol),
         terms: p.terms.into_iter().chain(q.terms).collect(),
     }))
 }
 
 fn conjoin_order_atoms(formula: fol::Formula, head_atom: fol::Atom) -> fol::Formula {
-    // replaces all positive atoms q(zs) in formula (i.e. all q(zs) not in the scope of any negation) by
-    // q(zs) and less_q_p(zs, xs)
+    // replaces all positive atoms q(zs) in formula
+    // (i.e. all q(zs) not in the scope of any negation) by
+    //   q(zs) and less_q_p(zs, xs)
     // where p(xs) is head_atom
     match formula {
         fol::Formula::AtomicFormula(fol::AtomicFormula::Atom(ref q)) => {