Thomas Sturm
001ece4cdd
A new, simpler rlsmt script
|
2 years ago | |
|---|---|---|
| .. | ||
| README | 2 years ago | |
| example1.smt2 | 2 years ago | |
| example2.smt2 | 2 years ago | |
| rlsmt | 2 years ago | |
README
rlsmt is a simple shell script for applying Redlog-based SMT solving to SMT-LIB 2 input files:
> rlsmt example1.smt2
sat
(
(define-fun v5 () Real
(@approximately 1.55685264521))
(define-fun v26 () Real
0)
(define-fun v137 () Real
(/ 1054143577565779 335544320000000))
)
> rlsmt example2.smt2
unsat
(0 1 10 8 3)
T. Sturm, November 2021
> rlsmt example1.smt2
sat
(
(define-fun v5 () Real
(@approximately 1.55685264521))
(define-fun v26 () Real
0)
(define-fun v137 () Real
(/ 1054143577565779 335544320000000))
)
> rlsmt example2.smt2
unsat
(0 1 10 8 3)
T. Sturm, November 2021