Small updates to cfa-cli readme

ftsrg · Sep 10, 2020 · 2ad2c31 · 2ad2c31
1 parent b7629d6
commit 2ad2c31
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/subprojects/cfa-cli/README.md b/subprojects/cfa-cli/README.md
@@ -83,11 +83,11 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J
     * `SEQ_ITP` (default): Sequence interpolation.
     * `MULTI_SEQ`: Sequence interpolation with multiple counterexamples (see Section 3.2.2 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information).
     * `UNSAT_CORE`: Simple unsat cores, only available if `--domain` is `EXPL`. This refinement strategy does not rely on interpolation, so it can even work if interpolating is not possible (e.g. bitvectors with Z3 solver).
-    * `UCB`: Unsat core based predicates [M. Leuckner et al.](https://link.springer.com/chapter/10.1007%2F978-3-319-26287-1_10). _Experimental feature._ This refinement strategy does not rely on interpolation, so it can even work if interpolating is not possible (e.g. bitvectors with Z3 solver).
-    * `NWT_*`: Newton-style refinement as per [D. Dietsch et al.](https://dl.acm.org/doi/10.1145/3106237.3106307). _Experimental feature._ This refinement strategy does not rely on interpolation, so it can even work if interpolating is not possible (e.g. bitvectors with Z3 solver). The supported Newton-style algorithms can be found in the following list (for more information on the algotithms, check the article):
-        * `NWT_SP` and `NWT_WP`: Only works for really simple inputs
-        * `NWT_SP_LV`, `NWT_WP_LV`, `NWT_IT_SP`, `NWT_IT_WP_LV`, `NWT_IT_SP_LV`
-        * `NWT_IT_WP`: Usually the most effective
+    * `UCB`: Unsat core based predicates ([see paper](https://link.springer.com/chapter/10.1007%2F978-3-319-26287-1_10) for more information). _Experimental feature._ Does not rely on interpolation, so it can even work if interpolating is not possible (e.g. bitvectors with Z3 solver).
+    * `NWT_*`: Newton-style refinement. _Experimental feature._ Does not rely on interpolation, so it can even work if interpolating is not possible (e.g. bitvectors with Z3 solver). The supported Newton-style variants can be found in the following list ([see paper](https://dl.acm.org/doi/10.1145/3106237.3106307) for more information):
+        * `NWT_SP` and `NWT_WP`: Only works for really simple inputs,
+        * `NWT_SP_LV`, `NWT_WP_LV`, `NWT_IT_SP`, `NWT_IT_WP_LV`, `NWT_IT_SP_LV`,
+        * `NWT_IT_WP`: Usually the most effective.
     * _Remark: `BW_BIN_ITP` and `SEQ_ITP` has the best performance usually. For bitvectors, `NWT_IT_WP` is recommended._
 * `--predsplit`: Splitting applied to predicates during refinement, possible values:
     * `WHOLE` (default): Keep predicates as a whole, no splitting is applied. Can perform well if the model has many Boolean variables.