Skip to content

Commit ca0ba17

Browse files
Merge pull request #22 from AdrienChampion/master
minor readme update
2 parents eddc37e + 2dd9f2e commit ca0ba17

File tree

1 file changed

+5
-7
lines changed

1 file changed

+5
-7
lines changed

README.md

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ It infers predicates verifying a set of horn clauses.
66
|:-------------:|:-------:|:---:|
77
| [![Build Status](https://travis-ci.org/hopv/hoice.svg?branch=master)](https://travis-ci.org/hopv/hoice) | [![Build status](https://ci.appveyor.com/api/projects/status/db247pe2jp9uo9cs?svg=true)](https://ci.appveyor.com/project/hopv/rsmt2) | [![codecov](https://codecov.io/gh/hopv/hoice/branch/master/graph/badge.svg)](https://codecov.io/gh/hopv/hoice) |
88

9-
`hoice` only supports the `Int` and `Bool` sorts. You can get a sense of the fragment `r_type` supports by looking at [our benchmarks][benchs].
9+
`hoice` supports the `Bool`, `Int` and `Real` sorts.
1010

1111
# Install
1212

@@ -18,13 +18,13 @@ Hoice generally uses the latest rust features available. Make sure the rust ecos
1818
rustup update stable
1919
```
2020

21-
Installing hoice with `cargo` installation:
21+
Installing hoice with `cargo`:
2222

2323
```bash
2424
cargo install --git https://github.com/hopv/hoice
2525
```
2626

27-
To build hoice manually, clone this repository `cd` in the directory and run
27+
To build hoice manually, clone this repository, `cd` in the directory and run
2828

2929
```bash
3030
cargo build --release
@@ -37,7 +37,7 @@ To get the fastest version, compile hoice with
3737
cargo build --release --features "bench"
3838
```
3939

40-
Note that this disables some features such as verbosity.
40+
Note that this disables some features such as verbose output, profiling...
4141

4242

4343
## z3
@@ -52,8 +52,7 @@ Note that this disables some features such as verbosity.
5252

5353
# Features
5454

55-
Sorts supported:
56-
55+
- [x] `define-fun`s
5756
- [x] `Bool`
5857
- [x] `Int`
5958
- [x] `Real`
@@ -63,7 +62,6 @@ Sorts supported:
6362

6463
Future features:
6564

66-
- [ ] `define-fun`s
6765
- [ ] user-specified qualifiers through `define-fun`s
6866

6967

0 commit comments

Comments
 (0)