Merge pull request #101 from VeriFIT/readme-update

Readme update
VeriFIT · Oct 2, 2023 · fb447e3 · fb447e3
2 parents f211b89 + ab40be9
commit fb447e3
Show file tree

Hide file tree

Showing 2 changed files with 56 additions and 54 deletions.
diff --git a/README-Starexec.md b/README-Starexec.md
@@ -0,0 +1,44 @@
+## Building and running on Starexec VM
+
+1. The VM:
+```
+VM: https://www.starexec.org/vmimage/
+user: root
+passwd: St@rexec
+```
+2. Install newer CMake:
+```shell
+git clone 'https://gitlab.kitware.com/cmake/cmake.git'
+cd cmake
+./configure
+gmake
+make install
+```
+3. Install Mata
+```shell
+git clone 'https://github.com/VeriFIT/mata.git'
+cd mata
+vim CMakeLists.txt
+# ... comment out the following two lines:
+#       include(CodeCoverage)
+#       setup_target_for_coverage(${PROJECT_NAME}_coverage tests coverage)
+CC=/opt/rh/devtoolset-8/root/usr/bin/gcc CXX=/opt/rh/devtoolset-8/root/usr/bin/g++ make release
+make install
+```
+4. Compile Noodler:
+
+```shell
+git clone 'https://github.com/VeriFIT/z3-noodler.git'
+mkdir z3-noodler/build
+cd z3-noodler/build
+vim ../src/test/CMakeLists.txt
+# ... comment out the following line:
+#       add_subdirectory(noodler)
+CC=/opt/rh/devtoolset-8/root/usr/bin/gcc CXX=/opt/rh/devtoolset-8/root/usr/bin/g++ cmake -DCMAKE_BUILD_TYPE=Release ..
+make
+```
+
+5. Now you should be able to run Z3-Noodler by typing
+```shell
+/root/z3-noodler/build/z3 smt.string_solver="noodler" <path/to/instance.smt2>
+```
diff --git a/README.md b/README.md
@@ -2,10 +2,8 @@
 
 Z3-Noodler is an SMT solver for string constraints such as those that occur in symbolic execution and analysis of programs, 
 reasoning about configuration files of cloud services and smart contracts, etc.
-Z3-Noodler is based on the SMT solver [Z3](https://github.com/Z3Prover/z3), in which it replaces the solver for the theory of strings. 
-The core of the string solver relies on the equation stabilization algorithm from the paper
-
-> F. Blahoudek, Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. [Word Equations in Synergy with Regular Constraints](https://link.springer.com/chapter/10.1007/978-3-031-27481-7_23).  In *Proc. of FM’23*, Lübeck, Germany, volume 14000 of LNCS, pages 403–423, 2023. Springer-Verlag.
+Z3-Noodler is based on the SMT solver [Z3 v4.12.2](https://github.com/Z3Prover/z3/releases/tag/z3-4.12.2), in which it replaces the solver for the theory of strings. 
+The core of the string solver implements several decision procedures, but mainly it relies on the equation stabilization algorithm (see [Publications](#publications)).
 
 Z3-Noodler utilizes the automata library [Mata](https://github.com/VeriFIT/mata/) for efficient representation of automata and their processing.
 
@@ -60,64 +58,23 @@ cd build/
 ```
 
 ## Limitations
-The following functions/predicates of the SMTLIB theory `Strings` are not supported at the moment.
+The following functions/predicates of the [SMTLIB Strings theory](https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml) are not supported at the moment.
 ```
+str.<
+str.<=
 str.replace_all
 str.replace_re
 str.replace_re_all
-str.is_digit
-str.to_code
-str.from_code
 str.to_int
 str.from_int
 ```
 
 We provide a full support for `str.contains`, but a limited support for its negated version.
 
-## Building and running on Starexec VM
-
-1. The VM:
-```
-VM: https://www.starexec.org/vmimage/
-user: root
-passwd: St@rexec
-```
-2. Install newer CMake:
-```shell
-git clone 'https://gitlab.kitware.com/cmake/cmake.git'
-cd cmake
-./configure
-gmake
-make install
-```
-3. Install Mata
-```shell
-git clone 'https://github.com/VeriFIT/mata.git'
-cd mata
-vim CMakeLists.txt
-# ... comment out the following two lines:
-#       include(CodeCoverage)
-#       setup_target_for_coverage(${PROJECT_NAME}_coverage tests coverage)
-CC=/opt/rh/devtoolset-8/root/usr/bin/gcc CXX=/opt/rh/devtoolset-8/root/usr/bin/g++ make release
-make install
-```
-4. Compile Noodler:
-
-```shell
-git clone 'https://github.com/VeriFIT/z3-noodler.git'
-mkdir z3-noodler/build
-cd z3-noodler/build
-vim ../src/test/CMakeLists.txt
-# ... comment out the following line:
-#       add_subdirectory(noodler)
-CC=/opt/rh/devtoolset-8/root/usr/bin/gcc CXX=/opt/rh/devtoolset-8/root/usr/bin/g++ cmake -DCMAKE_BUILD_TYPE=Release ..
-make
-```
+## Publications
+- Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. Solving String Constraints with Lengths by Stabilization. In *Proc. of OOPSLA'23*, Cascais, Portugal. 2023. ACM.
+- F. Blahoudek, Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. [Word Equations in Synergy with Regular Constraints](https://link.springer.com/chapter/10.1007/978-3-031-27481-7_23).  In *Proc. of FM’23*, Lübeck, Germany, volume 14000 of LNCS, pages 403–423, 2023. Springer-Verlag.
 
-5. Now you should be able to run Z3-Noodler by typing
-```shell
-/root/z3-noodler/build/z3 smt.string_solver="noodler" <path/to/instance.smt2>
-```
 
 ## Z3-Noodler source files
 
@@ -126,12 +83,13 @@ The string solver of Z3-Noodler is implemented in [src/smt/theory_str_noodler](s
 Tests for Z3-Noodler are located in [src/test/noodler](src/test/noodler).
 
 ## Authors
+- :envelope: [Vojtěch Havlena](mailto:ihavlena@fit.vut.cz?subject=[GitHub]%20Z3-Noodler),
+- :envelope: [Juraj Síč](mailto:sicjuraj@fit.vut.cz?subject=[GitHub]%20Z3-Noodler),
 - [Yu-Fang Chen](mailto:yfc@iis.sinica.edu.tw?subject=[GitHub]%20Z3-Noodler),
 - [David Chocholatý](mailto:xchoch08@stud.fit.vutbr.cz?subject=[GitHub]%20Z3-Noodler),
-- [Vojtěch Havlena](mailto:ihavlena@fit.vut.cz?subject=[GitHub]%20Z3-Noodler),
 - [Lukáš Holík](mailto:holik@fit.vut.cz?subject=[GitHub]%20Z3-Noodler),
-- [Ondřej Lengál](mailto:lengal@fit.vut.cz?subject=[GitHub]%20Z3-Noodler),
-- [Juraj Síč](mailto:sicjuraj@fit.vut.cz?subject=[GitHub]%20Z3-Noodler).
+- [Ondřej Lengál](mailto:lengal@fit.vut.cz?subject=[GitHub]%20Z3-Noodler).
+
 
 ## Original Z3 README