Skip to content

Commit 7a6277d

Browse files
Reformat documentation without latex
This is much more readable in the code, and still looks good in doxygen.
1 parent 0c56151 commit 7a6277d

File tree

1 file changed

+10
-10
lines changed

1 file changed

+10
-10
lines changed

src/solvers/refinement/string_constraint_generator_testing.cpp

+10-10
Original file line numberDiff line numberDiff line change
@@ -19,16 +19,16 @@ Author: Romain Brenguier, [email protected]
1919
/// second one, starting at position offset.
2020
///
2121
/// These axioms are:
22-
/// 1. \f$ {\tt isprefix} \Rightarrow {\tt offset_within_bounds}\f$
23-
/// 2. \f$ \forall 0 \le qvar<|{\tt prefix}|.\ {\tt isprefix}
24-
/// \Rightarrow s0[qvar+{\tt offset}]=s2[qvar] \f$
25-
/// 3. \f$ (\lnot {\tt isprefix} \Rightarrow
26-
/// \lnot {\tt offset_within_bounds}
27-
/// \lor (0 \le witness<|{\tt prefix}|
28-
/// \land {\tt str}[witness+{\tt offset}] \ne {\tt prefix}[witness])\f$
29-
/// where \f$ {\tt offset_within_bounds} \f$ is
30-
/// \f$ offset \ge 0 \land offset \le |str| \land
31-
/// |str| - offset \ge |{\tt prefix}| \f$
22+
/// 1. isprefix => offset_within_bounds
23+
/// 2. forall qvar in [0, |prefix|).
24+
/// isprefix => str[qvar + offset] = prefix[qvar]
25+
/// 3. !isprefix => !offset_within_bounds
26+
/// || 0 <= witness < |prefix|
27+
/// && str[witness+offset] != prefix[witness]
28+
///
29+
/// where offset_within_bounds is:
30+
/// offset >= 0 && offset <= |str| && |str| - offset >= |prefix|
31+
///
3232
/// \param prefix: an array of characters
3333
/// \param str: an array of characters
3434
/// \param offset: an integer

0 commit comments

Comments
 (0)