Interactive usage - Githubissues

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.

Apache License 2.0

84 stars 18 forks source link

Closed Vtec234 closed 2 years ago

Vtec234 commented 2 years ago

Closes #25.
Show error when the solver fails to solve the goal. I did not add close-goal-with-sorry for now.
Default solver.path to solver.kind, I was very confused as to why after setting the kind, CVC5 was still used.

abdoo8080 commented 2 years ago

btw, I am rewriting a new interface for the solver. So, don't spend time adding interactive features to the solver.

Vtec234 commented 2 years ago

btw, I am rewriting a new interface for the solver

The SolverM or something like it? Sounds good! A getModel call would be useful.