Skip to content

Commit

Permalink
interim
Browse files Browse the repository at this point in the history
  • Loading branch information
wintered committed Oct 18, 2024
1 parent 7673f2d commit 87279ed
Show file tree
Hide file tree
Showing 4 changed files with 6 additions and 5 deletions.
3 changes: 2 additions & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -24,9 +24,10 @@ jobs:
run: |
cabal install testing-feat
cabal install size-based
cabal install --lib size-based
- name: Test ET
run: |
bin/gen_tester grammars/Bitvectors.g4
#bin/run_tester 2 1000 Bitvectors solvers.cfg
bin/run_tester 2 100 Bitvectors solvers.cfg
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -57,15 +57,15 @@ the SMT solvers from `solvers.cfg` and differentially tests them.

## Usage

### 1. Generate tester
### Generate tester

```
bin/gen_tester grammars/Bitvectors.g4
```

This generates the executable bin/feat-Bitvectors.

### 2. Run tester
### Run tester

```
bin/run_tester 10 100000 Bitvectors solvers.cfg
Expand Down
2 changes: 1 addition & 1 deletion bin/gen_tester
Original file line number Diff line number Diff line change
Expand Up @@ -11,4 +11,4 @@ grammar_name=${grammar_name//.g4/}

etc/cfg2rtg $grammar_file > $grammar_name.hs
ghc $grammar_name.hs $FLAGS -o bin/feat-$grammar_name
#rm -rf $grammar_name.hi $grammar_name.o $grammar_name.hs
rm -rf $grammar_name.hi $grammar_name.o $grammar_name.hs
2 changes: 1 addition & 1 deletion solvers.cfg
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
z3 model_validate=true
cvc5 --strings-exp --check-unsat-cores --check-models -m -q
cvc4 --strings-exp --check-unsat-cores --check-models -m -q

0 comments on commit 87279ed

Please sign in to comment.