Highlight SMT capabilities in README

README.md

@@ -16,40 +16,22 @@ Run the project:
 `java -jar target/satchecking-1.0-SNAPSHOT.jar`  
 Now you should see the command prompt indicated by a `>` symbol.
 
-# Propositional logic
-A SAT solver is implemented that can
-employ [DPLL+CDCL](https://en.wikipedia.org/wiki/Conflict-driven_clause_learning), [DPLL](https://en.wikipedia.org/wiki/DPLL_algorithm)
-as well as simple enumeration to solve propositional logic problems.
-
-Input can be given in conjunctive normal form in the following way.
+# SMT solver
+An SMT solver is implemented for non-linear real arithmetic (QF_NRA), linear real arithmetic (QF_LRA), linear integer arithmetic (QF_LIA), equality logic (QF_EQ), equality logic with uninterpreted functions (QF_EQUF) and bit vector arithmetic (QF_BV).
 
+## Examples
+### QF_NRA: Non-linear real arithmetic with optimization
 ```c++
-> sat (a) & (~a | b) & (~b | ~c)
+> smt QF_NRA (y<=x^3) & (y<=-x^2+1) & (max(x+y))
 SAT:
-a=1, b=1, c=0;
-1 model/s found in 0 ms
+x=(x^3+x^2-1, 3/4, 7/8) ≈ 0.7548776662466928; y=(-1x^3+2x^2-3x+1, -4, 4) ≈ 0.4301597090019467;
+Time: 297ms
 ```
 ```c++
-> sat (a) & (~a | b) & (~b)
+> smt QF_NRA (x^2+y^2<1) & (min(y))
 UNSAT
+Time: 12ms
 ```
-
-# Tseitin's transformation
-The Tseitin transformation is implemented for propositional logic.
-It can be used to transform a formula into an equi-satisfiable formula in conjunctive normal form.
-The logical operators ``'~', '&', '|', '->', '<->'`` as well as parentheses are supported.
-
-```c++
-> tseitin ~(a & (a -> b) -> b)
-Tseitin's transformation:
-(~h3 | ~a | b) & (a | h3) & (~b | h3) & (~h2 | a) & (~h2 | h3) & (~a | ~h3 | h2) & (~h1 | ~h2 | b) & (h2 | h1) & (~b | h1) & (~h0 | ~h1) & (h1 | h0) & (h0)
-```
-
-# SMT solver
-An SMT solver is implemented for non-linear real arithmetic (QF_NRA), linear real arithmetic (QF_LRA), linear integer arithmetic (QF_LIA), equality logic (QF_EQ), equality logic with uninterpreted functions (QF_EQUF) and bit vector arithmetic (QF_BV).
-
-## Examples
-### QF_NRA (⚠️ highly experimental ⚠️)
 ```c++
 > smt QF_NRA (x^2 + y^2 = 1) & (x^2 + y^3 = 1/2)
 SAT:
@@ -61,20 +43,20 @@ Time: 456ms
 UNSAT
 Time: 7ms
 ```
-### QF_LRA
+### QF_LRA: Linear real arithmetic with optimization
 ```c++
-> smt QF_LRA (x<=-3 | x>=3) & (y=5) & (x+y>=12)
+> smt QF_LRA (x<=-3 | x>=3) & (y=5) & (x+y>=12) & (min(x))
 SAT:
 x=7; y=5;
-Time: 1ms
+Time: 0ms
 ```
 ```c++
 > smt QF_LRA (x<=0 | x>=5) & (x+y=5/2) & (y=1)
 UNSAT
 Time: 1ms
 ```
 
-### QF_LIA
+### QF_LIA: Linear integer arithmetic with optimization
 ```c++
 > smt QF_LIA (y+0.8x<=4) & (y-0.25x>=0) & (max(x))
 SAT:
@@ -87,7 +69,7 @@ UNSAT
 Time: 1ms
 ```
 
-### QF_EQ
+### QF_EQ: Equality logic
 ```c++
 > smt QF_EQ (a=b) & (c=d) & (a!=d)
 SAT:
@@ -100,7 +82,7 @@ UNSAT
 Time: 0ms
 ```
 
-### QF_EQUF
+### QF_EQUF: Equality logic with uninterpreted functions
 ```c++
 > smt QF_EQUF (x1 = x2) & (x2 = x3) & (x4 = x5) & (f(x1) != f(x5))
 SAT:
@@ -113,20 +95,48 @@ UNSAT
 Time: 0ms
 ```
 
-### QF_BV
+### QF_BV: Bit vector arithmetic
 ```c++
 > smt QF_BV (x >= 0) & (y > 0) & (y[6]) & (x >> y = 0) & (x + y < x * y)
 SAT:
 x=0b01010101 (85); y=0b01000000 (64);
 Time: 3ms
 ```
-
 ```c+++
 > smt QF_BV (a * b = c) & (b * a = c) & (x < y) & (y < x)
 UNSAT
 Time: 11ms
 ```
 
+# Propositional logic
+A SAT solver is implemented that can
+employ [DPLL+CDCL](https://en.wikipedia.org/wiki/Conflict-driven_clause_learning), [DPLL](https://en.wikipedia.org/wiki/DPLL_algorithm)
+as well as simple enumeration to solve propositional logic problems.
+
+Input can be given in conjunctive normal form in the following way.
+
+```c++
+> sat (a) & (~a | b) & (~b | ~c)
+SAT:
+a=1, b=1, c=0;
+1 model/s found in 0 ms
+```
+```c++
+> sat (a) & (~a | b) & (~b)
+UNSAT
+```
+
+# Tseitin's transformation
+The Tseitin transformation is implemented for propositional logic.
+It can be used to transform a formula into an equi-satisfiable formula in conjunctive normal form.
+The logical operators ``'~', '&', '|', '->', '<->'`` as well as parentheses are supported.
+
+```c++
+> tseitin ~(a & (a -> b) -> b)
+Tseitin's transformation:
+(~h3 | ~a | b) & (a | h3) & (~b | h3) & (~h2 | a) & (~h2 | h3) & (~a | ~h3 | h2) & (~h1 | ~h2 | b) & (h2 | h1) & (~b | h1) & (~h0 | ~h1) & (h1 | h0) & (h0)
+```
+
 # Theory solvers
 ## Linear real arithmetic (QF_LRA)
 The program can check sets of weak linear constraints for satisfiability employing