Support for bit-blasting about sbv HOT 3 CLOSED

Too low-level, and probably not worth it unless we also add support for loading AIG's back into SBV. This is best implemented outside of SBV probably, in a separate descendant package, if there's real need.

from sbv.

Apologies for resurrecting this old issue but what's the status of integration with ABC? Is it possible to bit blast an SBV expression into an AIG? I think SAW uses it so maybe it does exist but just in a different place.

from sbv.

ABC is supported by SBV; since they added basic support for SMTLib. You can use:

proveWith abc $ \x -> x + x .== 2 * (x::SWord8)

and it should work if you've a recent version of abc installed.

I should add that ABC's support for SMTLib format is rather limited; there are cases where it incorrectly parses the SMTLib format and does the wrong thing. (For instance, it does not support arrays.) If you stick to bit-vectors, it should more or less work just fine.

But otherwise, SBV does not support bit-blasting. Nor there are any plans for it. Let me know if the existing ABC interface gives you hard time!

from sbv.