Add remark in docs about forward interpolation

ftsrg · Jul 17, 2020 · de55f74 · de55f74
1 parent 44f596e
commit de55f74
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "1.2.0"
+    version = "1.3.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/cfa-cli/README.md b/subprojects/cfa-cli/README.md
@@ -64,7 +64,7 @@ If the limit is exceeded, unknown values are propagated.
 As a special case, `0` stands for infinite, but it should only be used if the model does not have any variable with unbounded domain.
 In general, values between `5` to `50` perform well (see Section 3.1.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information).
 - `--refinement`: Refinement strategy, possible values:
-  - `FW_BIN_ITP`: Forward binary interpolation, only a reference implementation, does not perform well.
+  - `FW_BIN_ITP`: Forward binary interpolation, only performs well if `--prunestrategy` is `FULL`.
   - `BW_BIN_ITP`: Backward binary interpolation (see Section 3.2.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information.
   - `SEQ_ITP`: 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).

diff --git a/subprojects/sts-cli/README.md b/subprojects/sts-cli/README.md
@@ -54,7 +54,7 @@ All arguments are optional, except `--model`.
 - `--search`: Search strategy in the abstract state space, possible values:
   - `BFS`, `DFS`: Standard breadth- and depth-first search.
 - `--refinement`: Refinement strategy, possible values:
-  - `FW_BIN_ITP`: Forward binary interpolation, only a reference implementation, does not perform well.
+  - `FW_BIN_ITP`: Forward binary interpolation, only performs well if `--prunestrategy` is `FULL`.
   - `BW_BIN_ITP`: Backward binary interpolation (see Section 3.2.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information.
   - `SEQ_ITP`: 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).