CVC5 fails to parse `what4`-generated SMT-LIB for constructing and selecting tuples

This program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Main where

import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Nonce as N
import qualified Data.Parameterized.Some as Some
import qualified System.IO as IO
import qualified What4.Config as WC
import qualified What4.Expr as WE
import qualified What4.Expr.Builder as WEB
import qualified What4.Expr.GroundEval as WEG
import qualified What4.Interface as WI
import qualified What4.Solver as WS

opts :: [WC.ConfigDesc]
opts = WS.cvc5Options

adapter :: WS.SolverAdapter st
adapter = WS.cvc5Adapter

main :: IO ()
main = do
  Some.Some ng <- N.newIONonceGenerator
  sym <- WEB.newExprBuilder WEB.FloatIEEERepr WE.EmptyExprBuilderState ng
  WC.extendConfig opts (WI.getConfiguration sym)

  let w = WI.knownNat @32
  ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn")
           (Ctx.Empty Ctx.:> WI.BaseStructRepr (Ctx.Empty Ctx.:> WI.BaseBVRepr w))
           (WI.BaseStructRepr (Ctx.Empty Ctx.:> WI.BaseBVRepr w))
  fldArg <- WI.freshConstant sym (WI.safeSymbol "fldArg") (WI.BaseBVRepr w)
  structArg <- WI.mkStruct sym (Ctx.Empty Ctx.:> fldArg)
  structRes <- WI.applySymFn sym ufn (Ctx.Empty Ctx.:> structArg)
  fldRes <- WI.structField sym structRes Ctx.baseIndex
  fldResNeg <- WI.bvNeg sym fldRes
  p <- WI.bvEq sym fldRes fldResNeg

  WS.solver_adapter_check_sat adapter sym
    WS.defaultLogData{WS.logHandle = Just IO.stdout} [p] $ \_result ->
    case _result of
      WS.Sat (ge, _) -> do
        putStrLn "Satisfiable, with model:"
        v <- WEG.groundEval ge fldArg
        putStrLn $ "fldArg := " ++ show v
      WS.Unsat _ -> putStrLn "Unsatisfiable."
      WS.Unknown -> putStrLn "Solver failed to find a solution."

Will fail with a CVC5-side parse error:

(set-logic ALL)
(set-option :produce-models true)
(set-option :produce-abducts true)
; :1:0
(declare-fun fldArg () (_ BitVec 32))
(define-fun x!0 () (Tuple (_ BitVec 32)) (mkTuple fldArg))
(declare-fun ufn ((Tuple (_ BitVec 32))) (Tuple (_ BitVec 32)))
(define-fun x!1 () (Tuple (_ BitVec 32)) (ufn x!0))
(define-fun x!2 () (_ BitVec 32) ((_ tupSel 0) x!1))
(define-fun x!3 () (_ BitVec 32) (bvneg x!2))
(define-fun x!4 () Bool (= x!2 x!3))
(assert x!4)
(check-sat)
; (error "Parse Error: <shell>:1.57: Symbol 'mkTuple' not declared as a variable")
*** Exception: Solver reported an error:
  Parse Error: <shell>:1.57: Symbol 'mkTuple' not declared as a variable
in response to command:
  (check-sat)

On the other hand, it will succeed if you change cvc5{Options,Adapter} to cvc4{Options,Adapter}. The reason this happens is because CVC4 and CVC5 have different operations to construct Tuples and to select individual Tuple fields. The CVC4 documentation says:

Tuples are a particular instance of an inductive datatype. CVC4 supports special syntax for tuples as an extension of the SMT-LIB version 2 format. For example:
(declare-fun t () (Tuple Int Int))
(assert (= ((_ tupSel 0) t) 3))
(assert (not (= t (mkTuple 3 4))))

In particular, it uses the mkTuple and tupSel constructs, and what4 uses these constructs when generating SMT-LIB for CVC4 to ingest.

When we added support for CVC5, we assumed that CVC5 used the same conventions as CVC4. This is mostly true, but not true in the particular case of tuples. The CVC5 documentation says:

Tuples are a particular instance of an inductive datatype. cvc5 supports special syntax for tuples as an extension of the SMT-LIB version 2 format. For example:
(declare-const t (Tuple Int Int))
(assert (= ((_ tuple.select 0) t) 3))
(assert (not (= t (tuple 3 4))))

Note that this now uses tuple instead of mkTuple and tuple.select instead of tupSel. We should use the same constructs when generating SMT-LIB for CVC5 to consume.

I was wondering how this bug managed to escape our testing. Then I took a look at the CVC5 tests, and I realized that we made a very embarrassing mistake:

what4/what4/test/ExprBuilderSMTLib2.hs

Line 1292 in 60cb3b8

let cvc5Tests = cvc4Tests

This isn't doing what we thought it did. Rather than repurposing the existing CVC4 tests to use CVC5 instead, this just runs the cvc4Tests twice (once as cvc4Tests, and once again as cvc5Tests).

After I fixed this oversight, I encountered this exact bug in some of the test cases (e.g., 0-tuple and 1-tuple). Luckily, fixing the bug above makes all of these test case failures go away.

Upon further investigation, making use of CVC5's tuple syntax is less straightforward than I realized. This is because in cvc5-1.0.9, the syntax for 1-ary tuples changed from Tuple to UnitTuple (cvc5/cvc5#10012), which means that we would have to generate different code on the what4 side if we wanted to support both pre- and post-1.0.9 versions of CVC5. Ugh.

Thankfully, it turns out we don't need the tuple workaround after all. Even further investigation reveals that the entire reason CVC4 uses tuples is to work around cvc5/cvc5#3402, but this issue doesn't affect CVC5 at all. As such, we can drop the tuple workaround for CVC5 (i.e., delete code) and everything just works.