search

FMFI-UK-1-AIN-412 / formalization-checker-backend

The back end of a tool for checking formalization exercises.
GNU General Public License v3.0
0 stars 5 forks source link

On-demand counterexamples and hints #36

Open crnkjck opened 1 year ago

crnkjck commented 1 year ago

Revert the check of formalization back to basic equivalence check. Add API endpoints for obtaining counter models and for obtaining hints. Rewrite front-end to call these asynchronously after obtaining the basic check result, or to get them only on explicit demand.

crnkjck commented 3 months ago

Consider caching the counter models to reduce usage of the theorem prover.