search

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
94 stars 19 forks source link

Refactor the Solver data-structure into a monad. #40

Closed abdoo8080 closed 2 years ago

abdoo8080 commented 2 years ago

The refactoring includes initial support for the get-model command and propagation of solver errors. The monad utilizes S-exprs (slightly modified) to communicate with the solver.