ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link

CHC solver access #632

Closed maul-esel closed 1 year ago

maul-esel commented 1 year ago

This PR allows access to several CHC solvers via a unified API. Solvers can be invoked via the IChcScript interface, or by including the ChcSolver plugin in the toolchain (the plugin just calls IChcScript methods internally). We have some support for extracting models (if SAT) and derivations or unsat cores (if UNSAT).

TODO

maul-esel commented 1 year ago

Setting unknownIsSuccess to true is indeed problematic, because we still want to test TreeAutomizer. Also, for unsupported features, exceptions are thrown -- which shouldn't count as UNKNOWN.

maul-esel commented 1 year ago

@danieldietsch: Sorry:

Screenshot from 2023-05-19 09-15-44

I still don't understand your issue with merge commits, though.

danieldietsch commented 1 year ago

@maul-esel ... we can discuss this, but if you like you can read, e.g., https://www.atlassian.com/git/tutorials/merging-vs-rebasing