search

wilbowma / cur

A less devious proof assistant
BSD 2-Clause "Simplified" License
220 stars 18 forks source link

Add some solvers! #48

Open wilbowma opened 8 years ago

wilbowma commented 8 years ago

SAT/SMT: https://planet.racket-lang.org/package-source/ianj/smt-solver.plt/1/1/planet-docs/smt-solver/An_SMT-solver_for_Racket.html#(def._((planet._smt-solve..rkt._(ianj._smt-solver..plt._1._0)._smt-solver)._smt-solve))

Systems of equations: https://docs.racket-lang.org/math/matrix_solve.html

diakopter commented 8 years ago

old, but I'm guessing not too difficult to un-bitrot..

https://github.com/sid0/z3.rkt

from the paper http://www.cse.iitk.ac.in/users/karkare/pubs/icsews13formalise-id1-p-16138-preprint.pdf

'course, it'd be nice to run/maintain z3 in-process, now that it's licensed much more permissively.