|
|
|
|
|
|
by c-cube
1568 days ago
|
|
|
It'd be great if it were less opaque, yes. SMT is a young field (early oughts) with a lot of extremely complicated algorithms jamed together, and there's not a lot of explanations beyond scientific papers. Even then, lots of topic required to implement a solver are not published at all, you need to know experts and ask them directly. The best way is of course to write a solver, but it's a tremendous amount of work to obtain a system that will most likely have bad performance, and where a single bug can invalidate the correctness of the whole program. Ask me how I know :-). People are working towards proof checking though, so that's at least going to help with trustability. |
|
|