Please enable JavaScript in your browser!
Почетна
Преглед
Помоћ
Регистрација
Пријавите се
reduce-algebra
/
reduce-algebra
огледало од
git://github.com/reduce-algebra/reduce-algebra
Прати
2
Волим
1
Креирај огранак
0
Датотеке
Дискусије
Грана:
master
Гране
Ознаке
master
svn/asau-bsd-port
svn/jaroschek
svn/sturm
reduce-algebra
/
generic
/
rlsmt
Thomas Sturm
001ece4cdd
A new, simpler rlsmt script
пре 2 година
..
README
001ece4cdd
A new, simpler rlsmt script
пре 2 година
example1.smt2
001ece4cdd
A new, simpler rlsmt script
пре 2 година
example2.smt2
001ece4cdd
A new, simpler rlsmt script
пре 2 година
rlsmt
001ece4cdd
A new, simpler rlsmt script
пре 2 година
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