search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Ensure that all (public) Boolector enums are accessible via the Python API #148

Closed aytey closed 3 years ago

aytey commented 3 years ago

Commit f69c12038bd2ccbc51593489dd67a35f113da3b7 moved a number of the Boolector enumerations from "internal" headers to being part of the public btortypes.h header.

Now that these enums are public, this PR exposes them via the Python API. It means that something like this:

import pyboolector

btor = pyboolector.Boolector()
sat_solver = "lingeling"
btor.Set_sat_solver(str(sat_solver))
assert (
    btor.Get_opt(pyboolector.BTOR_OPT_SAT_ENGINE).val
    == pyboolector.BTOR_SAT_ENGINE_LINGELING
)

is now possible when it previously was not.

Signed-off-by: Andrew V. Jones andrew.jones@vector.com