search

GaloisInc / what4

Symbolic formula representation and solver interaction library
155 stars 13 forks source link

CVC5: Don't use Tuple workaround when declaring structs #266

Closed RyanGlScott closed 5 months ago

RyanGlScott commented 5 months ago

Due to a bug in CVC4 (https://github.com/cvc5/cvc5/issues/3402), the What4 bindings to CVC4 avoid user-defined datatypes and instead use CVC4's built-in Tuple datatype. This same Tuple workaround was applied to the CVC5 bindings (added in https://github.com/GaloisInc/what4/pull/204), but they don't really work properly, as CVC4 and CVC5 use completely different syntaxes for tuples. See https://github.com/GaloisInc/what4/issues/265.

We could attempt to update the CVC5 bindings to use the modern tuple syntax, but this is somewhat non-trivial, as the syntax for 1-tuples changed in cvc5-1.0.9 from Tuple to UnitTuple (see https://github.com/cvc5/cvc5/pull/10012). As such, we would have to generate different code for different versions of CVC5, which would be unpleasant.

Thankfully, we need not worry about tuples at all when it comes to CVC5. This is because the original CVC4 issue (https://github.com/cvc5/cvc5/issues/3402) does not affect CVC5. As such, we can drop the tuple workaround entirely and just generate user-defined datatypes to represent What4 structs, exactly like the other solver bindings do. This means that we can fix https://github.com/GaloisInc/what4/issues/265 by simply deleting code, which is nice.

In addition, this PR tweaks the expr-builder-smtlib2 test suite to actually run its tests with both CVC4 and CVC5. The 0-tuple and 1-tuple tests catch the exact bug described in #265, so these serve as a regression test for #265 when run with CVC5.

Fixes https://github.com/GaloisInc/what4/issues/265.

RyanGlScott commented 5 months ago

I don't think so. CVC5 does in fact use structs—that fact remains unchanged by this PR. The only difference is how it implements structs under the hood: it used tuples before, but now it uses user-defined datatypes.