As title says, a simple solver utilizing the internal evaluator to discharge VCs is added.
On non-ground assertions, Unknown is returned. On successfully verifying an assertion, i.e. evaluating it to true, if a model was requested, an empty model (Map.empty) is returned. This is the expected model for a ground query.
Correspondingly, if the assertion evaluates to false, Unsat is returned.
The evaluator itself is tested in both Inox and Stainless, so not duplicating those tests. I have a small set of integration tests for the solver (that pass with this build), which I will add to benchmarks/ in Stainless after this is merged.
As title says, a simple solver utilizing the internal evaluator to discharge VCs is added.
On non-ground assertions,
Unknownis returned. On successfully verifying an assertion, i.e. evaluating it totrue, if a model was requested, an empty model (Map.empty) is returned. This is the expected model for a ground query.Correspondingly, if the assertion evaluates to
false,Unsatis returned.The evaluator itself is tested in both Inox and Stainless, so not duplicating those tests. I have a small set of integration tests for the solver (that pass with this build), which I will add to
benchmarks/in Stainless after this is merged.