    ------------------------------------------------------------------------
    -- |
    -- Module      : What4.Solver.Yices
    -- Description : Solver adapter code for Yices
    -- Copyright   : (c) Galois, Inc 2015-2020
    -- License     : BSD3
    -- Maintainer  : Rob Dockins <rdockins@galois.com>
    -- Stability   : provisional
    --
    -- SMTWriter interface for Yices, using the Yices-specific input language.
    -- This language shares many features with SMTLib2, but is not quite
    -- compatible.
    ------------------------------------------------------------------------

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DoAndIfThenElse #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE Rank2Types #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE ViewPatterns #-}
    module What4.Solver.Yices
      ( -- * Low-level interface
        Connection
      , newConnection
      , SMTWriter.assume
      , sendCheck
      , sendCheckExistsForall
      , eval
      , push
      , pop
      , inNewFrame
      , setParam
      , setYicesParams
      , HandleReader
      , startHandleReader

      , yicesType
      , assertForall
      , efSolveCommand
      , YicesException(..)

        -- * Live connection
      , yicesEvalBool
      , SMTWriter.addCommand

        -- * Solver adapter interface
      , yicesAdapter
      , runYicesInOverride
      , writeYicesFile
      , yicesPath
      , yicesOptions
      , yicesDefaultFeatures
      , yicesEnableMCSat
      , yicesEnableInteractive
      , yicesGoalTimeout
      ) where

    #if !MIN_VERSION_base(4,13,0)
    import           Control.Monad.Fail ( MonadFail )
    #endif

    import           Control.Applicative
    import           Control.Concurrent ( threadDelay )
    import           Control.Concurrent.Async ( race )
    import           Control.Exception
                       (assert, SomeException(..), tryJust, throw, displayException, Exception(..))
    import           Control.Lens ((^.), folded)
    import           Control.Monad
    import           Control.Monad.Identity
    import qualified Data.Attoparsec.Text as Atto
    import           Data.Bits
    import qualified Data.BitVector.Sized as BV

    import           Data.IORef
    import           Data.Foldable (toList)
    import           Data.Maybe
    import qualified Data.Parameterized.Context as Ctx
    import           Data.Parameterized.NatRepr
    import           Data.Parameterized.Some
    import           Data.Parameterized.TraversableFC
    import           Data.Ratio
    import           Data.Set (Set)
    import qualified Data.Set as Set
    import           Data.String (fromString)
    import           Data.Text (Text)
    import qualified Data.Text as Text
    import qualified Data.Text.Lazy as Lazy
    import           Data.Text.Lazy.Builder (Builder)
    import qualified Data.Text.Lazy.Builder as Builder
    import           Data.Text.Lazy.Builder.Int (decimal)
    import           Numeric (readOct)
    import           System.Exit
    import           System.IO
    import qualified System.IO.Streams as Streams
    import qualified System.IO.Streams.Attoparsec.Text as Streams
    import qualified Prettyprinter as PP

    import           What4.BaseTypes
    import           What4.Concrete
    import           What4.Config
    import qualified What4.Expr.Builder as B
    import           What4.Expr.GroundEval
    import           What4.Expr.VarIdentification
    import           What4.Interface
    import           What4.ProblemFeatures
    import           What4.Protocol.Online
    import qualified What4.Protocol.PolyRoot as Root
    import           What4.Protocol.SExp
    import           What4.Protocol.SMTLib2 (writeDefaultSMT2)
    import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
    import           What4.Protocol.SMTWriter as SMTWriter
    import           What4.SatResult
    import           What4.Solver.Adapter
    import           What4.Utils.HandleReader
    import           What4.Utils.Process

    import           Prelude
    import           GHC.Stack

    -- | This is a tag used to indicate that a 'WriterConn' is a connection
    -- to a specific Yices process.
    data Connection = Connection
      { Connection -> IORef (Maybe Int)
    yicesEarlyUnsat :: IORef (Maybe Int)
      , Connection -> SolverGoalTimeout
    yicesTimeout :: SolverGoalTimeout
      , Connection -> IORef Bool
    yicesUnitDeclared :: IORef Bool
      }

    -- | Attempt to interpret a Config value as a Yices value.
    asYicesConfigValue :: ConcreteVal tp -> Maybe Builder
    asYicesConfigValue :: forall (tp :: BaseType). ConcreteVal tp -> Maybe Builder
    asYicesConfigValue ConcreteVal tp
    v = case ConcreteVal tp
    v of
      ConcreteBool Bool
    x ->
          Builder -> Maybe Builder
    forall a. a -> Maybe a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (if Bool
    x then Builder
    "true" else Builder
    "false")
      ConcreteReal Rational
    x ->
          Builder -> Maybe Builder
    forall a. a -> Maybe a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Builder -> Maybe Builder) -> Builder -> Maybe Builder
    forall a b. (a -> b) -> a -> b
    $ Integer -> Builder
    forall a. Integral a => a -> Builder
    decimal (Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    x) Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    "/" Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Integer -> Builder
    forall a. Integral a => a -> Builder
    decimal (Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    x)
      ConcreteInteger Integer
    x ->
          Builder -> Maybe Builder
    forall a. a -> Maybe a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Builder -> Maybe Builder) -> Builder -> Maybe Builder
    forall a b. (a -> b) -> a -> b
    $ Integer -> Builder
    forall a. Integral a => a -> Builder
    decimal Integer
    x
      ConcreteString (UnicodeLiteral Text
    x) ->
          Builder -> Maybe Builder
    forall a. a -> Maybe a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Builder -> Maybe Builder) -> Builder -> Maybe Builder
    forall a b. (a -> b) -> a -> b
    $ Text -> Builder
    Builder.fromText Text
    x
      ConcreteVal tp
    _ ->
          Maybe Builder
    forall a. Maybe a
    Nothing

    ------------------------------------------------------------------------
    -- Expr

    newtype YicesTerm = T { YicesTerm -> Builder
    renderTerm :: Builder }

    term_app :: Builder -> [YicesTerm] -> YicesTerm
    term_app :: Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    o [YicesTerm]
    args = Builder -> YicesTerm
    T (Builder -> [Builder] -> Builder
    app Builder
    o (YicesTerm -> Builder
    renderTerm (YicesTerm -> Builder) -> [YicesTerm] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [YicesTerm]
    args))

    bin_app :: Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app :: Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    o YicesTerm
    x YicesTerm
    y = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    o [YicesTerm
    x,YicesTerm
    y]

    type Expr = YicesTerm

    instance Num YicesTerm where
      + :: YicesTerm -> YicesTerm -> YicesTerm
    (+) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "+"
      (-) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "-"
      * :: YicesTerm -> YicesTerm -> YicesTerm
    (*) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "*"
      negate :: YicesTerm -> YicesTerm
    negate YicesTerm
    x = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "-" [YicesTerm
    x]
      abs :: YicesTerm -> YicesTerm
    abs YicesTerm
    x    = YicesTerm -> YicesTerm -> YicesTerm -> YicesTerm
    forall v. SupportTermOps v => v -> v -> v -> v
    ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    ">=" YicesTerm
    x YicesTerm
    0) YicesTerm
    x (YicesTerm -> YicesTerm
    forall a. Num a => a -> a
    negate YicesTerm
    x)
      signum :: YicesTerm -> YicesTerm
    signum YicesTerm
    x = YicesTerm -> YicesTerm -> YicesTerm -> YicesTerm
    forall v. SupportTermOps v => v -> v -> v -> v
    ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "=" YicesTerm
    x YicesTerm
    0) YicesTerm
    0 (YicesTerm -> YicesTerm) -> YicesTerm -> YicesTerm
    forall a b. (a -> b) -> a -> b
    $ YicesTerm -> YicesTerm -> YicesTerm -> YicesTerm
    forall v. SupportTermOps v => v -> v -> v -> v
    ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    ">" YicesTerm
    x YicesTerm
    0) YicesTerm
    1 (YicesTerm -> YicesTerm
    forall a. Num a => a -> a
    negate YicesTerm
    1)
      fromInteger :: Integer -> YicesTerm
    fromInteger Integer
    i = Builder -> YicesTerm
    T (Integer -> Builder
    forall a. Integral a => a -> Builder
    decimal Integer
    i)

    decimal_term :: Integral a => a -> YicesTerm
    decimal_term :: forall a. Integral a => a -> YicesTerm
    decimal_term a
    i = Builder -> YicesTerm
    T (a -> Builder
    forall a. Integral a => a -> Builder
    decimal a
    i)

    width_term :: NatRepr n -> YicesTerm
    width_term :: forall (n :: Nat). NatRepr n -> YicesTerm
    width_term NatRepr n
    w = Int -> YicesTerm
    forall a. Integral a => a -> YicesTerm
    decimal_term (NatRepr n -> Int
    forall (n :: Nat). NatRepr n -> Int
    widthVal NatRepr n
    w)

    varBinding :: Text -> Some TypeMap -> Builder
    varBinding :: Text -> Some TypeMap -> Builder
    varBinding Text
    nm Some TypeMap
    tp = Text -> Builder
    Builder.fromText Text
    nm Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    "::" Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> YicesType -> Builder
    unType ((forall (tp :: BaseType). TypeMap tp -> YicesType)
    -> Some TypeMap -> YicesType
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome TypeMap tp -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType Some TypeMap
    tp)

    letBinding :: Text -> YicesTerm -> Builder
    letBinding :: Text -> YicesTerm -> Builder
    letBinding Text
    nm YicesTerm
    t = Builder -> [Builder] -> Builder
    app (Text -> Builder
    Builder.fromText Text
    nm) [YicesTerm -> Builder
    renderTerm YicesTerm
    t]

    binder_app :: Builder -> [Builder] -> YicesTerm -> YicesTerm
    binder_app :: Builder -> [Builder] -> YicesTerm -> YicesTerm
    binder_app Builder
    _  []    YicesTerm
    t = YicesTerm
    t
    binder_app Builder
    nm (Builder
    h:[Builder]
    r) YicesTerm
    t = Builder -> YicesTerm
    T (Builder -> [Builder] -> Builder
    app Builder
    nm [Builder -> [Builder] -> Builder
    app_list Builder
    h [Builder]
    r, YicesTerm -> Builder
    renderTerm YicesTerm
    t])

    yicesLambda :: [(Text, Some TypeMap)] -> YicesTerm -> YicesTerm
    yicesLambda :: [(Text, Some TypeMap)] -> YicesTerm -> YicesTerm
    yicesLambda []   YicesTerm
    t = YicesTerm
    t
    yicesLambda [(Text, Some TypeMap)]
    args YicesTerm
    t = Builder -> YicesTerm
    T (Builder -> YicesTerm) -> Builder -> YicesTerm
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "lambda" [ [Builder] -> Builder
    builder_list ((Text -> Some TypeMap -> Builder)
    -> (Text, Some TypeMap) -> Builder
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Text -> Some TypeMap -> Builder
    varBinding ((Text, Some TypeMap) -> Builder)
    -> [(Text, Some TypeMap)] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Text, Some TypeMap)]
    args), YicesTerm -> Builder
    renderTerm YicesTerm
    t ]

    instance SupportTermOps YicesTerm where
      boolExpr :: Bool -> YicesTerm
    boolExpr Bool
    b = Builder -> YicesTerm
    T (Builder -> YicesTerm) -> Builder -> YicesTerm
    forall a b. (a -> b) -> a -> b
    $ if Bool
    b then Builder
    "true" else Builder
    "false"
      notExpr :: YicesTerm -> YicesTerm
    notExpr YicesTerm
    x = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "not" [YicesTerm
    x]

      andAll :: [YicesTerm] -> YicesTerm
    andAll [] = Builder -> YicesTerm
    T Builder
    "true"
      andAll [YicesTerm
    x] = YicesTerm
    x
      andAll [YicesTerm]
    xs = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "and" [YicesTerm]
    xs

      orAll :: [YicesTerm] -> YicesTerm
    orAll [] = Builder -> YicesTerm
    T Builder
    "false"
      orAll [YicesTerm
    x] = YicesTerm
    x
      orAll [YicesTerm]
    xs = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "or" [YicesTerm]
    xs

      .== :: YicesTerm -> YicesTerm -> YicesTerm
    (.==) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "="
      ./= :: YicesTerm -> YicesTerm -> YicesTerm
    (./=) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "/="
      ite :: YicesTerm -> YicesTerm -> YicesTerm -> YicesTerm
    ite YicesTerm
    c YicesTerm
    x YicesTerm
    y = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "if" [YicesTerm
    c, YicesTerm
    x, YicesTerm
    y]

      -- NB: Yices "let" has the semantics of a sequential let, so no
      -- transformations need to be done
      letExpr :: [(Text, YicesTerm)] -> YicesTerm -> YicesTerm
    letExpr [(Text, YicesTerm)]
    vars YicesTerm
    t = Builder -> [Builder] -> YicesTerm -> YicesTerm
    binder_app Builder
    "let" ((Text -> YicesTerm -> Builder) -> (Text, YicesTerm) -> Builder
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Text -> YicesTerm -> Builder
    letBinding ((Text, YicesTerm) -> Builder) -> [(Text, YicesTerm)] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Text, YicesTerm)]
    vars) YicesTerm
    t

      sumExpr :: [YicesTerm] -> YicesTerm
    sumExpr [] = YicesTerm
    0
      sumExpr [YicesTerm
    e] = YicesTerm
    e
      sumExpr [YicesTerm]
    l = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "+" [YicesTerm]
    l

      termIntegerToReal :: YicesTerm -> YicesTerm
    termIntegerToReal = YicesTerm -> YicesTerm
    forall a. a -> a
    id
      termRealToInteger :: YicesTerm -> YicesTerm
    termRealToInteger = YicesTerm -> YicesTerm
    forall a. a -> a
    id

      integerTerm :: Integer -> YicesTerm
    integerTerm Integer
    i = Builder -> YicesTerm
    T (Builder -> YicesTerm) -> Builder -> YicesTerm
    forall a b. (a -> b) -> a -> b
    $ Integer -> Builder
    forall a. Integral a => a -> Builder
    decimal Integer
    i

      intDiv :: YicesTerm -> YicesTerm -> YicesTerm
    intDiv YicesTerm
    x YicesTerm
    y = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "div" [YicesTerm
    x,YicesTerm
    y]
      intMod :: YicesTerm -> YicesTerm -> YicesTerm
    intMod YicesTerm
    x YicesTerm
    y = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "mod" [YicesTerm
    x,YicesTerm
    y]
      intAbs :: YicesTerm -> YicesTerm
    intAbs YicesTerm
    x   = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "abs" [YicesTerm
    x]

      intDivisible :: YicesTerm -> Nat -> YicesTerm
    intDivisible YicesTerm
    x Nat
    0 = YicesTerm
    x YicesTerm -> YicesTerm -> YicesTerm
    forall v. SupportTermOps v => v -> v -> v
    .== Integer -> YicesTerm
    forall v. SupportTermOps v => Integer -> v
    integerTerm Integer
    0
      intDivisible YicesTerm
    x Nat
    k = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "divides" [Integer -> YicesTerm
    forall v. SupportTermOps v => Integer -> v
    integerTerm (Nat -> Integer
    forall a. Integral a => a -> Integer
    toInteger Nat
    k), YicesTerm
    x]

      rationalTerm :: Rational -> YicesTerm
    rationalTerm Rational
    r | Integer
    d Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1    = Builder -> YicesTerm
    T (Builder -> YicesTerm) -> Builder -> YicesTerm
    forall a b. (a -> b) -> a -> b
    $ Integer -> Builder
    forall a. Integral a => a -> Builder
    decimal Integer
    n
                     | Bool
    otherwise = Builder -> YicesTerm
    T (Builder -> YicesTerm) -> Builder -> YicesTerm
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "/" [Integer -> Builder
    forall a. Integral a => a -> Builder
    decimal Integer
    n, Integer -> Builder
    forall a. Integral a => a -> Builder
    decimal Integer
    d]
        where n :: Integer
    n = Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    r
              d :: Integer
    d = Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    r

      .< :: YicesTerm -> YicesTerm -> YicesTerm
    (.<)  = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "<"
      .<= :: YicesTerm -> YicesTerm -> YicesTerm
    (.<=) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "<="
      .> :: YicesTerm -> YicesTerm -> YicesTerm
    (.>)  = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    ">"
      .>= :: YicesTerm -> YicesTerm -> YicesTerm
    (.>=) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    ">="

      bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> YicesTerm
    bvTerm NatRepr w
    w BV w
    u = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "mk-bv" [NatRepr w -> YicesTerm
    forall (n :: Nat). NatRepr n -> YicesTerm
    width_term NatRepr w
    w, Integer -> YicesTerm
    forall a. Integral a => a -> YicesTerm
    decimal_term Integer
    d]
        where d :: Integer
    d = BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    u

      bvNeg :: YicesTerm -> YicesTerm
    bvNeg YicesTerm
    x = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "bv-neg" [YicesTerm
    x]
      bvAdd :: YicesTerm -> YicesTerm -> YicesTerm
    bvAdd = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-add"
      bvSub :: YicesTerm -> YicesTerm -> YicesTerm
    bvSub = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-sub"
      bvMul :: YicesTerm -> YicesTerm -> YicesTerm
    bvMul = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-mul"

      bvSLe :: YicesTerm -> YicesTerm -> YicesTerm
    bvSLe = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-sle"
      bvULe :: YicesTerm -> YicesTerm -> YicesTerm
    bvULe = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-le"

      bvSLt :: YicesTerm -> YicesTerm -> YicesTerm
    bvSLt = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-slt"
      bvULt :: YicesTerm -> YicesTerm -> YicesTerm
    bvULt = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-lt"

      bvUDiv :: YicesTerm -> YicesTerm -> YicesTerm
    bvUDiv = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-div"
      bvURem :: YicesTerm -> YicesTerm -> YicesTerm
    bvURem = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-rem"
      bvSDiv :: YicesTerm -> YicesTerm -> YicesTerm
    bvSDiv = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-sdiv"
      bvSRem :: YicesTerm -> YicesTerm -> YicesTerm
    bvSRem = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-srem"

      bvAnd :: YicesTerm -> YicesTerm -> YicesTerm
    bvAnd  = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-and"
      bvOr :: YicesTerm -> YicesTerm -> YicesTerm
    bvOr   = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-or"
      bvXor :: YicesTerm -> YicesTerm -> YicesTerm
    bvXor  = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-xor"

      bvNot :: YicesTerm -> YicesTerm
    bvNot YicesTerm
    x = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "bv-not" [YicesTerm
    x]

      bvShl :: YicesTerm -> YicesTerm -> YicesTerm
    bvShl  = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-shl"
      bvLshr :: YicesTerm -> YicesTerm -> YicesTerm
    bvLshr = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-lshr"
      bvAshr :: YicesTerm -> YicesTerm -> YicesTerm
    bvAshr = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-ashr"

      -- Yices concatenates with least significant bit first.
      bvConcat :: YicesTerm -> YicesTerm -> YicesTerm
    bvConcat YicesTerm
    x YicesTerm
    y = Builder -> YicesTerm -> YicesTerm -> YicesTerm
    bin_app Builder
    "bv-concat" YicesTerm
    x YicesTerm
    y

      bvExtract :: forall (w :: Nat).
    NatRepr w -> Nat -> Nat -> YicesTerm -> YicesTerm
    bvExtract NatRepr w
    _ Nat
    b Nat
    n YicesTerm
    x = Bool -> YicesTerm -> YicesTerm
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    0) (YicesTerm -> YicesTerm) -> YicesTerm -> YicesTerm
    forall a b. (a -> b) -> a -> b
    $
        let -- Get index of bit to end at (least-significant bit has index 0)
            end :: YicesTerm
    end = Nat -> YicesTerm
    forall a. Integral a => a -> YicesTerm
    decimal_term (Nat
    bNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    +Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1)
            -- Get index of bit to start at (least-significant bit has index 0)
            begin :: YicesTerm
    begin = Nat -> YicesTerm
    forall a. Integral a => a -> YicesTerm
    decimal_term Nat
    b
         in Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "bv-extract"  [YicesTerm
    end, YicesTerm
    begin, YicesTerm
    x]

      realIsInteger :: YicesTerm -> YicesTerm
    realIsInteger YicesTerm
    x = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "is-int" [YicesTerm
    x]

      realDiv :: YicesTerm -> YicesTerm -> YicesTerm
    realDiv YicesTerm
    x YicesTerm
    y = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "/" [YicesTerm
    x, YicesTerm
    y]
      realSin :: YicesTerm -> YicesTerm
    realSin = YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported
      realCos :: YicesTerm -> YicesTerm
    realCos = YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported
      realTan :: YicesTerm -> YicesTerm
    realTan = YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported
      realATan2 :: YicesTerm -> YicesTerm -> YicesTerm
    realATan2 = YicesTerm -> YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported
      realSinh :: YicesTerm -> YicesTerm
    realSinh = YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported
      realCosh :: YicesTerm -> YicesTerm
    realCosh = YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported
      realTanh :: YicesTerm -> YicesTerm
    realTanh = YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported
      realExp :: YicesTerm -> YicesTerm
    realExp = YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported
      realLog :: YicesTerm -> YicesTerm
    realLog = YicesTerm -> YicesTerm
    forall a. a
    errorComputableUnsupported

      smtFnApp :: YicesTerm -> [YicesTerm] -> YicesTerm
    smtFnApp YicesTerm
    nm [YicesTerm]
    args = Builder -> [YicesTerm] -> YicesTerm
    term_app (YicesTerm -> Builder
    renderTerm YicesTerm
    nm) [YicesTerm]
    args
      smtFnUpdate :: Maybe (YicesTerm -> [YicesTerm] -> YicesTerm -> YicesTerm)
    smtFnUpdate = Maybe (YicesTerm -> [YicesTerm] -> YicesTerm -> YicesTerm)
    forall a. Maybe a
    Nothing

      lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> YicesTerm -> YicesTerm)
    lambdaTerm = ([(Text, Some TypeMap)] -> YicesTerm -> YicesTerm)
    -> Maybe ([(Text, Some TypeMap)] -> YicesTerm -> YicesTerm)
    forall a. a -> Maybe a
    Just [(Text, Some TypeMap)] -> YicesTerm -> YicesTerm
    yicesLambda

      floatTerm :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BigFloat -> YicesTerm
    floatTerm FloatPrecisionRepr fpp
    _ BigFloat
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail

      floatNeg :: YicesTerm -> YicesTerm
    floatNeg  YicesTerm
    _   = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatAbs :: YicesTerm -> YicesTerm
    floatAbs  YicesTerm
    _   = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatSqrt :: RoundingMode -> YicesTerm -> YicesTerm
    floatSqrt RoundingMode
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail

      floatAdd :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm
    floatAdd RoundingMode
    _ YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatSub :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm
    floatSub RoundingMode
    _ YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatMul :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm
    floatMul RoundingMode
    _ YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatDiv :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm
    floatDiv RoundingMode
    _ YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatRem :: YicesTerm -> YicesTerm -> YicesTerm
    floatRem YicesTerm
    _ YicesTerm
    _   = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail

      floatFMA :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm -> YicesTerm
    floatFMA RoundingMode
    _ YicesTerm
    _ YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail

      floatEq :: YicesTerm -> YicesTerm -> YicesTerm
    floatEq   YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatFpEq :: YicesTerm -> YicesTerm -> YicesTerm
    floatFpEq YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatLe :: YicesTerm -> YicesTerm -> YicesTerm
    floatLe   YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatLt :: YicesTerm -> YicesTerm -> YicesTerm
    floatLt   YicesTerm
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail

      floatIsNaN :: YicesTerm -> YicesTerm
    floatIsNaN     YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatIsInf :: YicesTerm -> YicesTerm
    floatIsInf     YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatIsZero :: YicesTerm -> YicesTerm
    floatIsZero    YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatIsPos :: YicesTerm -> YicesTerm
    floatIsPos     YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatIsNeg :: YicesTerm -> YicesTerm
    floatIsNeg     YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatIsSubnorm :: YicesTerm -> YicesTerm
    floatIsSubnorm YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatIsNorm :: YicesTerm -> YicesTerm
    floatIsNorm    YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail

      floatCast :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
    floatCast       FloatPrecisionRepr fpp
    _ RoundingMode
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatRound :: RoundingMode -> YicesTerm -> YicesTerm
    floatRound      RoundingMode
    _ YicesTerm
    _   = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatFromBinary :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> YicesTerm -> YicesTerm
    floatFromBinary FloatPrecisionRepr fpp
    _ YicesTerm
    _   = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      bvToFloat :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
    bvToFloat       FloatPrecisionRepr fpp
    _ RoundingMode
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      sbvToFloat :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
    sbvToFloat      FloatPrecisionRepr fpp
    _ RoundingMode
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      realToFloat :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
    realToFloat     FloatPrecisionRepr fpp
    _ RoundingMode
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatToBV :: Nat -> RoundingMode -> YicesTerm -> YicesTerm
    floatToBV       Nat
    _ RoundingMode
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatToSBV :: Nat -> RoundingMode -> YicesTerm -> YicesTerm
    floatToSBV      Nat
    _ RoundingMode
    _ YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail
      floatToReal :: YicesTerm -> YicesTerm
    floatToReal     YicesTerm
    _ = YicesTerm
    forall a. (?callStack::CallStack) => a
    floatFail

      fromText :: Text -> YicesTerm
    fromText Text
    t = Builder -> YicesTerm
    T (Text -> Builder
    Builder.fromText Text
    t)

    unsupportedFeature :: String -> a
    unsupportedFeature :: forall a. [Char] -> a
    unsupportedFeature [Char]
    s = [Char] -> a
    forall a. (?callStack::CallStack) => [Char] -> a
    error ([Char]
    "Yices does not support " [Char] -> [Char] -> [Char]
    forall a. Semigroup a => a -> a -> a
    <> [Char]
    s)

    floatFail :: HasCallStack => a
    floatFail :: forall a. (?callStack::CallStack) => a
    floatFail = [Char] -> a
    forall a. (?callStack::CallStack) => [Char] -> a
    error [Char]
    "Yices does not support IEEE-754 floating-point numbers"

    stringFail :: HasCallStack => a
    stringFail :: forall a. (?callStack::CallStack) => a
    stringFail = [Char] -> a
    forall a. (?callStack::CallStack) => [Char] -> a
    error [Char]
    "Yices does not support strings"

    errorComputableUnsupported :: a
    errorComputableUnsupported :: forall a. a
    errorComputableUnsupported = [Char] -> a
    forall a. (?callStack::CallStack) => [Char] -> a
    error [Char]
    "computable functions are not supported."

    ------------------------------------------------------------------------
    -- YicesType

    -- | Denotes a type in yices.
    newtype YicesType = YicesType { YicesType -> Builder
    unType :: Builder }

    tupleType :: [YicesType] -> YicesType
    tupleType :: [YicesType] -> YicesType
    tupleType []   = Builder -> YicesType
    YicesType Builder
    "unit-type"
    tupleType [YicesType]
    flds = Builder -> YicesType
    YicesType (Builder -> [Builder] -> Builder
    app Builder
    "tuple" (YicesType -> Builder
    unType (YicesType -> Builder) -> [YicesType] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [YicesType]
    flds))

    boolType :: YicesType
    boolType :: YicesType
    boolType = Builder -> YicesType
    YicesType Builder
    "bool"

    intType :: YicesType
    intType :: YicesType
    intType = Builder -> YicesType
    YicesType Builder
    "int"

    realType :: YicesType
    realType :: YicesType
    realType = Builder -> YicesType
    YicesType Builder
    "real"

    fnType :: [YicesType] -> YicesType -> YicesType
    fnType :: [YicesType] -> YicesType -> YicesType
    fnType [] YicesType
    tp = YicesType
    tp
    fnType [YicesType]
    args YicesType
    tp = Builder -> YicesType
    YicesType (Builder -> YicesType) -> Builder -> YicesType
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "->" (YicesType -> Builder
    unType (YicesType -> Builder) -> [YicesType] -> [Builder]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` ([YicesType]
    args [YicesType] -> [YicesType] -> [YicesType]
    forall a. [a] -> [a] -> [a]
    ++ [YicesType
    tp]))

    yicesType :: TypeMap tp -> YicesType
    yicesType :: forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType TypeMap tp
    BoolTypeMap    = YicesType
    boolType
    yicesType TypeMap tp
    IntegerTypeMap = YicesType
    intType
    yicesType TypeMap tp
    RealTypeMap    = YicesType
    realType
    yicesType (BVTypeMap NatRepr w
    w)  = Builder -> YicesType
    YicesType (Builder -> [Builder] -> Builder
    app Builder
    "bitvector" [[Char] -> Builder
    forall a. IsString a => [Char] -> a
    fromString (NatRepr w -> [Char]
    forall a. Show a => a -> [Char]
    show NatRepr w
    w)])
    yicesType (FloatTypeMap FloatPrecisionRepr fpp
    _) = YicesType
    forall a. (?callStack::CallStack) => a
    floatFail
    yicesType TypeMap tp
    UnicodeTypeMap = YicesType
    forall a. (?callStack::CallStack) => a
    stringFail
    yicesType TypeMap tp
    ComplexToStructTypeMap = [YicesType] -> YicesType
    tupleType [YicesType
    realType, YicesType
    realType]
    yicesType TypeMap tp
    ComplexToArrayTypeMap  = [YicesType] -> YicesType -> YicesType
    fnType [YicesType
    boolType] YicesType
    realType
    yicesType (PrimArrayTypeMap Assignment TypeMap (idxl ::> idx)
    i TypeMap tp1
    r) = [YicesType] -> YicesType -> YicesType
    fnType ((forall (tp :: BaseType). TypeMap tp -> YicesType)
    -> forall (x :: Ctx BaseType). Assignment TypeMap x -> [YicesType]
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    toListFC TypeMap x -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType Assignment TypeMap (idxl ::> idx)
    i) (TypeMap tp1 -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType TypeMap tp1
    r)
    yicesType (FnArrayTypeMap Assignment TypeMap (idxl ::> idx)
    i TypeMap tp1
    r)   = [YicesType] -> YicesType -> YicesType
    fnType ((forall (tp :: BaseType). TypeMap tp -> YicesType)
    -> forall (x :: Ctx BaseType). Assignment TypeMap x -> [YicesType]
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    toListFC TypeMap x -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType Assignment TypeMap (idxl ::> idx)
    i) (TypeMap tp1 -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType TypeMap tp1
    r)
    yicesType (StructTypeMap Assignment TypeMap idx
    f)      = [YicesType] -> YicesType
    tupleType ((forall (tp :: BaseType). TypeMap tp -> YicesType)
    -> forall (x :: Ctx BaseType). Assignment TypeMap x -> [YicesType]
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    toListFC TypeMap x -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType Assignment TypeMap idx
    f)

    ------------------------------------------------------------------------
    -- Command

    assertForallCommand :: [(Text,YicesType)] -> Expr -> Command Connection
    assertForallCommand :: [(Text, YicesType)] -> YicesTerm -> Command Connection
    assertForallCommand [(Text, YicesType)]
    vars YicesTerm
    e = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    unsafeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "assert" [YicesTerm -> Builder
    renderTerm YicesTerm
    res]
     where res :: YicesTerm
    res = Builder -> [Builder] -> YicesTerm -> YicesTerm
    binder_app Builder
    "forall" ((Text -> YicesType -> Builder) -> (Text, YicesType) -> Builder
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Text -> YicesType -> Builder
    mkBinding ((Text, YicesType) -> Builder) -> [(Text, YicesType)] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Text, YicesType)]
    vars) YicesTerm
    e
           mkBinding :: Text -> YicesType -> Builder
    mkBinding Text
    nm YicesType
    tp = Text -> Builder
    Builder.fromText Text
    nm Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    "::" Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> YicesType -> Builder
    unType YicesType
    tp

    efSolveCommand :: Command Connection
    efSolveCommand :: Command Connection
    efSolveCommand Connection
    _ = Builder -> YicesCommand
    safeCmd Builder
    "(ef-solve)"

    evalCommand :: Term Connection -> Command Connection
    evalCommand :: Term Connection -> Command Connection
    evalCommand Term Connection
    v Connection
    _ = Builder -> YicesCommand
    safeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "eval" [YicesTerm -> Builder
    renderTerm Term Connection
    YicesTerm
    v]

    exitCommand :: Command Connection
    exitCommand :: Command Connection
    exitCommand Connection
    _ = Builder -> YicesCommand
    safeCmd Builder
    "(exit)"

    -- | Tell yices to show a model
    showModelCommand :: Command Connection
    showModelCommand :: Command Connection
    showModelCommand Connection
    _ = Builder -> YicesCommand
    safeCmd Builder
    "(show-model)"

    checkExistsForallCommand :: Command Connection
    checkExistsForallCommand :: Command Connection
    checkExistsForallCommand Connection
    _ = Builder -> YicesCommand
    safeCmd Builder
    "(ef-solve)"

    -- | Create yices set command value.
    setParamCommand :: Text -> Builder -> Command Connection
    setParamCommand :: Text -> Builder -> Command Connection
    setParamCommand Text
    nm Builder
    v Connection
    _ = Builder -> YicesCommand
    safeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "set-param" [ Text -> Builder
    Builder.fromText Text
    nm, Builder
    v ]

    setTimeoutCommand :: Command Connection
    setTimeoutCommand :: Command Connection
    setTimeoutCommand Connection
    conn = Builder -> YicesCommand
    unsafeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $
       Builder -> [Builder] -> Builder
    app Builder
    "set-timeout" [ [Char] -> Builder
    Builder.fromString (Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (SolverGoalTimeout -> Integer
    getGoalTimeoutInSeconds (SolverGoalTimeout -> Integer) -> SolverGoalTimeout -> Integer
    forall a b. (a -> b) -> a -> b
    $ Connection -> SolverGoalTimeout
    yicesTimeout Connection
    conn)) ]

    declareUnitTypeCommand :: Command Connection
    declareUnitTypeCommand :: Command Connection
    declareUnitTypeCommand Connection
    _conn = Builder -> YicesCommand
    safeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $
      Builder -> [Builder] -> Builder
    app Builder
    "define-type" [ [Char] -> Builder
    Builder.fromString [Char]
    "unit-type", Builder -> [Builder] -> Builder
    app Builder
    "scalar" [ [Char] -> Builder
    Builder.fromString [Char]
    "unit-value" ] ]

    declareUnitType :: WriterConn t Connection -> IO ()
    declareUnitType :: forall t. WriterConn t Connection -> IO ()
    declareUnitType WriterConn t Connection
    conn =
      do done <- IORef Bool -> (Bool -> (Bool, Bool)) -> IO Bool
    forall a b. IORef a -> (a -> (a, b)) -> IO b
    atomicModifyIORef (Connection -> IORef Bool
    yicesUnitDeclared (WriterConn t Connection -> Connection
    forall t h. WriterConn t h -> h
    connState WriterConn t Connection
    conn)) (\Bool
    x -> (Bool
    True, Bool
    x))
         unless done $ addCommand conn declareUnitTypeCommand

    resetUnitType :: WriterConn t Connection -> IO ()
    resetUnitType :: forall t. WriterConn t Connection -> IO ()
    resetUnitType WriterConn t Connection
    conn =
      IORef Bool -> Bool -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (Connection -> IORef Bool
    yicesUnitDeclared (WriterConn t Connection -> Connection
    forall t h. WriterConn t h -> h
    connState WriterConn t Connection
    conn)) Bool
    False

    ------------------------------------------------------------------------
    -- Connection

    newConnection ::
      Streams.OutputStream Text ->
      Streams.InputStream Text ->
      (IORef (Maybe Int) -> AcknowledgementAction t Connection) ->
      ProblemFeatures {- ^ Indicates the problem features to support. -} ->
      SolverGoalTimeout ->
      B.SymbolVarBimap t ->
      IO (WriterConn t Connection)
    newConnection :: forall t.
    OutputStream Text
    -> InputStream Text
    -> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
    -> ProblemFeatures
    -> SolverGoalTimeout
    -> SymbolVarBimap t
    -> IO (WriterConn t Connection)
    newConnection OutputStream Text
    stream InputStream Text
    in_stream IORef (Maybe Int) -> AcknowledgementAction t Connection
    ack ProblemFeatures
    reqFeatures SolverGoalTimeout
    timeout SymbolVarBimap t
    bindings = do
      let efSolver :: Bool
    efSolver = ProblemFeatures
    reqFeatures ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useExistForall
      let nlSolver :: Bool
    nlSolver = ProblemFeatures
    reqFeatures ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useNonlinearArithmetic
      let features :: ProblemFeatures
    features | Bool
    efSolver  = ProblemFeatures
    useLinearArithmetic
                   | Bool
    nlSolver  = ProblemFeatures
    useNonlinearArithmetic ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useIntegerArithmetic
                   | Bool
    otherwise = ProblemFeatures
    reqFeatures
      let nm :: [Char]
    nm | Bool
    efSolver  = [Char]
    "Yices ef-solver"
             | Bool
    nlSolver  = [Char]
    "Yices nl-solver"
             | Bool
    otherwise = [Char]
    "Yices"
      let featureIf :: Bool -> ProblemFeatures -> ProblemFeatures
    featureIf Bool
    True ProblemFeatures
    f = ProblemFeatures
    f
          featureIf Bool
    False ProblemFeatures
    _ = ProblemFeatures
    noFeatures
      let features' :: ProblemFeatures
    features' = ProblemFeatures
    features
                      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. Bool -> ProblemFeatures -> ProblemFeatures
    featureIf Bool
    efSolver ProblemFeatures
    useExistForall
                      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useStructs
                      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. (ProblemFeatures
    reqFeatures ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .&. (ProblemFeatures
    useUnsatCores ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useUnsatAssumptions))

      earlyUnsatRef <- Maybe Int -> IO (IORef (Maybe Int))
    forall a. a -> IO (IORef a)
    newIORef Maybe Int
    forall a. Maybe a
    Nothing
      unitRef <- newIORef False
      let c = Connection { yicesEarlyUnsat :: IORef (Maybe Int)
    yicesEarlyUnsat = IORef (Maybe Int)
    earlyUnsatRef
                         , yicesTimeout :: SolverGoalTimeout
    yicesTimeout = SolverGoalTimeout
    timeout
                         , yicesUnitDeclared :: IORef Bool
    yicesUnitDeclared = IORef Bool
    unitRef
                         }
      conn <- newWriterConn stream in_stream (ack earlyUnsatRef) nm Strict features' bindings c
      return $! conn { supportFunctionDefs = True
                     , supportFunctionArguments = True
                     , supportQuantifiers = efSolver
                     }

    -- | This data type bundles a Yices command (as a Text Builder) with an
    -- indication as to whether it is safe to issue in an inconsistent
    -- context. Unsafe commands are the ones that Yices will complain about
    -- to stderr if issued, causing interaction to hang.
    data YicesCommand = YicesCommand
      { YicesCommand -> Bool
    cmdEarlyUnsatSafe :: Bool
      , YicesCommand -> Builder
    cmdCmd :: Builder
      }

    safeCmd :: Builder -> YicesCommand
    safeCmd :: Builder -> YicesCommand
    safeCmd Builder
    txt = YicesCommand { cmdEarlyUnsatSafe :: Bool
    cmdEarlyUnsatSafe = Bool
    True, cmdCmd :: Builder
    cmdCmd = Builder
    txt }

    unsafeCmd :: Builder -> YicesCommand
    unsafeCmd :: Builder -> YicesCommand
    unsafeCmd Builder
    txt = YicesCommand { cmdEarlyUnsatSafe :: Bool
    cmdEarlyUnsatSafe = Bool
    False, cmdCmd :: Builder
    cmdCmd = Builder
    txt }

    type instance Term Connection = YicesTerm
    type instance Command Connection = Connection -> YicesCommand

    instance SMTWriter Connection where
      forallExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection
    forallExpr [(Text, Some TypeMap)]
    vars Term Connection
    t = Builder -> [Builder] -> YicesTerm -> YicesTerm
    binder_app Builder
    "forall" ((Text -> Some TypeMap -> Builder)
    -> (Text, Some TypeMap) -> Builder
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Text -> Some TypeMap -> Builder
    varBinding ((Text, Some TypeMap) -> Builder)
    -> [(Text, Some TypeMap)] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Text, Some TypeMap)]
    vars) Term Connection
    YicesTerm
    t
      existsExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection
    existsExpr [(Text, Some TypeMap)]
    vars Term Connection
    t = Builder -> [Builder] -> YicesTerm -> YicesTerm
    binder_app Builder
    "exists" ((Text -> Some TypeMap -> Builder)
    -> (Text, Some TypeMap) -> Builder
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Text -> Some TypeMap -> Builder
    varBinding ((Text, Some TypeMap) -> Builder)
    -> [(Text, Some TypeMap)] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Text, Some TypeMap)]
    vars) Term Connection
    YicesTerm
    t

      arraySelect :: Term Connection -> [Term Connection] -> Term Connection
    arraySelect = Term Connection -> [Term Connection] -> Term Connection
    YicesTerm -> [YicesTerm] -> YicesTerm
    forall v. SupportTermOps v => v -> [v] -> v
    smtFnApp
      arrayUpdate :: Term Connection
    -> [Term Connection] -> Term Connection -> Term Connection
    arrayUpdate Term Connection
    a [Term Connection]
    i Term Connection
    v =
        Builder -> YicesTerm
    T (Builder -> YicesTerm) -> Builder -> YicesTerm
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "update" [ YicesTerm -> Builder
    renderTerm Term Connection
    YicesTerm
    a, [Builder] -> Builder
    builder_list (YicesTerm -> Builder
    renderTerm (YicesTerm -> Builder) -> [YicesTerm] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Term Connection]
    [YicesTerm]
    i), YicesTerm -> Builder
    renderTerm Term Connection
    YicesTerm
    v ]

      commentCommand :: forall (f :: Type -> Type).
    f Connection -> Builder -> Command Connection
    commentCommand f Connection
    _ Builder
    b = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd (Builder
    ";; " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    b)

      pushCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
    pushCommand f Connection
    _   = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd Builder
    "(push)"
      popCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
    popCommand f Connection
    _    = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd Builder
    "(pop)"
      push2Command :: forall (f :: Type -> Type). f Connection -> Command Connection
    push2Command f Connection
    _   = [Char] -> Connection -> YicesCommand
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "(push 2)"
      pop2Command :: forall (f :: Type -> Type). f Connection -> Command Connection
    pop2Command f Connection
    _    = [Char] -> Connection -> YicesCommand
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "(pop 2)"
      resetCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
    resetCommand f Connection
    _  = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd Builder
    "(reset)"
      checkCommands :: forall (f :: Type -> Type). f Connection -> [Command Connection]
    checkCommands f Connection
    _  =
        [ Command Connection
    setTimeoutCommand, YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd Builder
    "(check)" ]
      checkWithAssumptionsCommands :: forall (f :: Type -> Type).
    f Connection -> [Text] -> [Command Connection]
    checkWithAssumptionsCommands f Connection
    _ [Text]
    nms =
        [ Command Connection
    setTimeoutCommand
        , YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app_list Builder
    "check-assuming" ((Text -> Builder) -> [Text] -> [Builder]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> Builder
    Builder.fromText [Text]
    nms)
        ]

      getUnsatAssumptionsCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
    getUnsatAssumptionsCommand f Connection
    _ = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd Builder
    "(show-unsat-assumptions)"
      getUnsatCoreCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
    getUnsatCoreCommand f Connection
    _ = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd Builder
    "(show-unsat-core)"
      getAbductCommand :: forall (f :: Type -> Type).
    f Connection -> Text -> Term Connection -> Command Connection
    getAbductCommand f Connection
    _ Text
    _ Term Connection
    _ = [Char] -> Connection -> YicesCommand
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "abduction"
      getAbductNextCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
    getAbductNextCommand f Connection
    _ = [Char] -> Connection -> YicesCommand
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "abduction"

      setOptCommand :: forall (f :: Type -> Type).
    f Connection -> Text -> Text -> Command Connection
    setOptCommand f Connection
    _ Text
    x Text
    o = Text -> Builder -> Command Connection
    setParamCommand Text
    x (Text -> Builder
    Builder.fromText Text
    o)

      assertCommand :: forall (f :: Type -> Type).
    f Connection -> Term Connection -> Command Connection
    assertCommand f Connection
    _ (T Builder
    nm) = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    unsafeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "assert" [Builder
    nm]
      assertNamedCommand :: forall (f :: Type -> Type).
    f Connection -> Term Connection -> Text -> Command Connection
    assertNamedCommand f Connection
    _ (T Builder
    tm) Text
    nm = YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    unsafeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "assert" [Builder
    tm, Text -> Builder
    Builder.fromText Text
    nm]

      declareCommand :: forall (f :: Type -> Type) (args :: Ctx BaseType)
           (rtp :: BaseType).
    f Connection
    -> Text
    -> Assignment TypeMap args
    -> TypeMap rtp
    -> Command Connection
    declareCommand f Connection
    _ Text
    v Assignment TypeMap args
    args TypeMap rtp
    rtp =
        YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $
        Builder -> [Builder] -> Builder
    app Builder
    "define" [Text -> Builder
    Builder.fromText Text
    v Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    "::"
                      Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> YicesType -> Builder
    unType ([YicesType] -> YicesType -> YicesType
    fnType ((forall (tp :: BaseType). TypeMap tp -> YicesType)
    -> forall (x :: Ctx BaseType). Assignment TypeMap x -> [YicesType]
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    toListFC TypeMap x -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType Assignment TypeMap args
    args) (TypeMap rtp -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType TypeMap rtp
    rtp))
                     ]

      defineCommand :: forall (f :: Type -> Type) (rtp :: BaseType).
    f Connection
    -> Text
    -> [(Text, Some TypeMap)]
    -> TypeMap rtp
    -> Term Connection
    -> Command Connection
    defineCommand f Connection
    _ Text
    v [(Text, Some TypeMap)]
    args TypeMap rtp
    rtp Term Connection
    t =
        YicesCommand -> Connection -> YicesCommand
    forall a b. a -> b -> a
    const (YicesCommand -> Connection -> YicesCommand)
    -> YicesCommand -> Connection -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $ Builder -> YicesCommand
    safeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
    forall a b. (a -> b) -> a -> b
    $
        Builder -> [Builder] -> Builder
    app Builder
    "define" [Text -> Builder
    Builder.fromText Text
    v Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    "::"
                      Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> YicesType -> Builder
    unType ([YicesType] -> YicesType -> YicesType
    fnType ((\(Text
    _,Some TypeMap
    tp) -> (forall (tp :: BaseType). TypeMap tp -> YicesType)
    -> Some TypeMap -> YicesType
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome TypeMap tp -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType Some TypeMap
    tp) ((Text, Some TypeMap) -> YicesType)
    -> [(Text, Some TypeMap)] -> [YicesType]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Text, Some TypeMap)]
    args) (TypeMap rtp -> YicesType
    forall (tp :: BaseType). TypeMap tp -> YicesType
    yicesType TypeMap rtp
    rtp))
                     , YicesTerm -> Builder
    renderTerm ([(Text, Some TypeMap)] -> YicesTerm -> YicesTerm
    yicesLambda [(Text, Some TypeMap)]
    args Term Connection
    YicesTerm
    t)
                     ]

      synthFunCommand :: forall (f :: Type -> Type) (tp :: BaseType).
    f Connection
    -> Text
    -> [(Text, Some TypeMap)]
    -> TypeMap tp
    -> Command Connection
    synthFunCommand f Connection
    _ Text
    _ [(Text, Some TypeMap)]
    _ TypeMap tp
    _ = [Char] -> Connection -> YicesCommand
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "SyGuS"
      declareVarCommand :: forall (f :: Type -> Type) (tp :: BaseType).
    f Connection -> Text -> TypeMap tp -> Command Connection
    declareVarCommand f Connection
    _ Text
    _ TypeMap tp
    _ = [Char] -> Connection -> YicesCommand
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "SyGuS"
      constraintCommand :: forall (f :: Type -> Type).
    f Connection -> Term Connection -> Command Connection
    constraintCommand f Connection
    _ Term Connection
    _ = [Char] -> Connection -> YicesCommand
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "SyGuS"

      resetDeclaredStructs :: forall t. WriterConn t Connection -> IO ()
    resetDeclaredStructs WriterConn t Connection
    conn = WriterConn t Connection -> IO ()
    forall t. WriterConn t Connection -> IO ()
    resetUnitType WriterConn t Connection
    conn

      structProj :: forall (args :: Ctx BaseType) (tp :: BaseType).
    Assignment TypeMap args
    -> Index args tp -> Term Connection -> Term Connection
    structProj Assignment TypeMap args
    _n Index args tp
    i Term Connection
    s = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "select" [Term Connection
    YicesTerm
    s, Int -> YicesTerm
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Index args tp -> Int
    forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
    Ctx.indexVal Index args tp
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)]

      structCtor :: forall (args :: Ctx BaseType).
    Assignment TypeMap args -> [Term Connection] -> Term Connection
    structCtor Assignment TypeMap args
    _tps []   = Builder -> YicesTerm
    T Builder
    "unit-value"
      structCtor Assignment TypeMap args
    _tps [Term Connection]
    args = Builder -> [YicesTerm] -> YicesTerm
    term_app Builder
    "mk-tuple" [Term Connection]
    [YicesTerm]
    args

      stringTerm :: Text -> Term Connection
    stringTerm Text
    _   = Term Connection
    YicesTerm
    forall a. (?callStack::CallStack) => a
    stringFail
      stringLength :: Term Connection -> Term Connection
    stringLength Term Connection
    _ = Term Connection
    YicesTerm
    forall a. (?callStack::CallStack) => a
    stringFail
      stringAppend :: [Term Connection] -> Term Connection
    stringAppend [Term Connection]
    _ = Term Connection
    YicesTerm
    forall a. (?callStack::CallStack) => a
    stringFail
      stringContains :: Term Connection -> Term Connection -> Term Connection
    stringContains Term Connection
    _ Term Connection
    _ = Term Connection
    YicesTerm
    forall a. (?callStack::CallStack) => a
    stringFail
      stringIndexOf :: Term Connection
    -> Term Connection -> Term Connection -> Term Connection
    stringIndexOf Term Connection
    _ Term Connection
    _ Term Connection
    _ = Term Connection
    YicesTerm
    forall a. (?callStack::CallStack) => a
    stringFail
      stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection
    stringIsPrefixOf Term Connection
    _ Term Connection
    _ = Term Connection
    YicesTerm
    forall a. (?callStack::CallStack) => a
    stringFail
      stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection
    stringIsSuffixOf Term Connection
    _ Term Connection
    _ = Term Connection
    YicesTerm
    forall a. (?callStack::CallStack) => a
    stringFail
      stringSubstring :: Term Connection
    -> Term Connection -> Term Connection -> Term Connection
    stringSubstring Term Connection
    _ Term Connection
    _ Term Connection
    _ = Term Connection
    YicesTerm
    forall a. (?callStack::CallStack) => a
    stringFail

      -- yices has built-in syntax for n-tuples where n > 0,
      -- so we only need to delcare the unit type for 0-tuples
      declareStructDatatype :: forall t (args :: Ctx BaseType).
    WriterConn t Connection -> Assignment TypeMap args -> IO ()
    declareStructDatatype WriterConn t Connection
    conn Assignment TypeMap args
    Ctx.Empty = WriterConn t Connection -> IO ()
    forall t. WriterConn t Connection -> IO ()
    declareUnitType WriterConn t Connection
    conn
      declareStructDatatype WriterConn t Connection
    _ Assignment TypeMap args
    _ = () -> IO ()
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()

      writeCommand :: forall t. WriterConn t Connection -> Command Connection -> IO ()
    writeCommand WriterConn t Connection
    conn Command Connection
    cmdf =
        do isEarlyUnsat <- IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef (Connection -> IORef (Maybe Int)
    yicesEarlyUnsat (WriterConn t Connection -> Connection
    forall t h. WriterConn t h -> h
    connState WriterConn t Connection
    conn))
           unless (isJust isEarlyUnsat && not earlyUnsatSafe) $ do
             Streams.write (Just cmdout) (connHandle conn)
             -- force a flush
             Streams.write (Just "") (connHandle conn)
        where
          cmd :: YicesCommand
    cmd = Command Connection
    Connection -> YicesCommand
    cmdf (WriterConn t Connection -> Connection
    forall t h. WriterConn t h -> h
    connState WriterConn t Connection
    conn)
          earlyUnsatSafe :: Bool
    earlyUnsatSafe = YicesCommand -> Bool
    cmdEarlyUnsatSafe YicesCommand
    cmd
          cmdBuilder :: Builder
    cmdBuilder = YicesCommand -> Builder
    cmdCmd YicesCommand
    cmd
          cmdout :: Text
    cmdout = LazyText -> Text
    Lazy.toStrict (Builder -> LazyText
    Builder.toLazyText Builder
    cmdBuilder) Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "\n"

    instance SMTReadWriter Connection where
      smtEvalFuns :: forall t.
    WriterConn t Connection
    -> InputStream Text -> SMTEvalFunctions Connection
    smtEvalFuns WriterConn t Connection
    conn InputStream Text
    resp =
        SMTEvalFunctions { smtEvalBool :: Term Connection -> IO Bool
    smtEvalBool    = Eval t Bool
    forall s. Eval s Bool
    yicesEvalBool WriterConn t Connection
    conn InputStream Text
    resp
                         , smtEvalBV :: forall (w :: Nat). NatRepr w -> Term Connection -> IO (BV w)
    smtEvalBV      = \NatRepr w
    w -> NatRepr w -> Eval t (BV w)
    forall (w :: Nat) s. NatRepr w -> Eval s (BV w)
    yicesEvalBV NatRepr w
    w WriterConn t Connection
    conn InputStream Text
    resp
                         , smtEvalReal :: Term Connection -> IO Rational
    smtEvalReal    = Eval t Rational
    forall s. Eval s Rational
    yicesEvalReal WriterConn t Connection
    conn InputStream Text
    resp
                         , smtEvalFloat :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp
    -> Term Connection -> IO (BV (FloatPrecisionBits fpp))
    smtEvalFloat   = \FloatPrecisionRepr fpp
    _ Term Connection
    _ -> [Char] -> IO (BV (FloatPrecisionBits fpp))
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail [Char]
    "Yices does not support floats."
                         , smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper Connection)
    smtEvalBvArray = Maybe (SMTEvalBVArrayWrapper Connection)
    forall a. Maybe a
    Nothing
                         , smtEvalString :: Term Connection -> IO Text
    smtEvalString  = \Term Connection
    _ -> [Char] -> IO Text
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail [Char]
    "Yices does not support strings."
                         }

      smtSatResult :: forall (f :: Type -> Type) t.
    f Connection -> WriterConn t Connection -> IO (SatResult () ())
    smtSatResult f Connection
    _ = WriterConn t Connection -> IO (SatResult () ())
    forall t. WriterConn t Connection -> IO (SatResult () ())
    getSatResponse

      smtUnsatAssumptionsResult :: forall (f :: Type -> Type) t.
    f Connection -> WriterConn t Connection -> IO [(Bool, Text)]
    smtUnsatAssumptionsResult f Connection
    _ WriterConn t Connection
    s =
        do mb <- (SomeException -> Maybe SomeException)
    -> IO SExp -> IO (Either SomeException SExp)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (Parser SExp -> InputStream Text -> IO SExp
    forall r. Parser r -> InputStream Text -> IO r
    Streams.parseFromStream (Parser Text -> Parser SExp
    parseSExp Parser Text
    parseYicesString) (WriterConn t Connection -> InputStream Text
    forall t h. WriterConn t h -> InputStream Text
    connInputHandle WriterConn t Connection
    s))
           let cmd = Builder -> YicesCommand
    safeCmd Builder
    "(show-unsat-assumptions)"
           case mb of
             Right (SExp -> Maybe [(Bool, Text)]
    asNegAtomList -> Just [(Bool, Text)]
    as) -> [(Bool, Text)] -> IO [(Bool, Text)]
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return [(Bool, Text)]
    as
             Right (SApp [SAtom Text
    "error", SString Text
    msg]) -> YicesException -> IO [(Bool, Text)]
    forall a e. (?callStack::CallStack, Exception e) => e -> a
    throw (YicesCommand -> Text -> YicesException
    YicesError YicesCommand
    cmd Text
    msg)
             Right SExp
    res -> YicesException -> IO [(Bool, Text)]
    forall a e. (?callStack::CallStack, Exception e) => e -> a
    throw (YicesCommand -> Text -> YicesException
    YicesParseError YicesCommand
    cmd ([Char] -> Text
    Text.pack (SExp -> [Char]
    forall a. Show a => a -> [Char]
    show SExp
    res)))
             Left (SomeException e
    e) -> YicesException -> IO [(Bool, Text)]
    forall a e. (?callStack::CallStack, Exception e) => e -> a
    throw (YicesException -> IO [(Bool, Text)])
    -> YicesException -> IO [(Bool, Text)]
    forall a b. (a -> b) -> a -> b
    $ YicesCommand -> Text -> YicesException
    YicesParseError YicesCommand
    cmd (Text -> YicesException) -> Text -> YicesException
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Text
    Text.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $
                     [[Char]] -> [Char]
    unlines [ [Char]
    "Could not parse unsat assumptions result."
                             , [Char]
    "*** Exception: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ e -> [Char]
    forall e. Exception e => e -> [Char]
    displayException e
    e
                             ]

      smtUnsatCoreResult :: forall (f :: Type -> Type) t.
    f Connection -> WriterConn t Connection -> IO [Text]
    smtUnsatCoreResult f Connection
    _ WriterConn t Connection
    s =
        do mb <- (SomeException -> Maybe SomeException)
    -> IO SExp -> IO (Either SomeException SExp)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (Parser SExp -> InputStream Text -> IO SExp
    forall r. Parser r -> InputStream Text -> IO r
    Streams.parseFromStream (Parser Text -> Parser SExp
    parseSExp Parser Text
    parseYicesString) (WriterConn t Connection -> InputStream Text
    forall t h. WriterConn t h -> InputStream Text
    connInputHandle WriterConn t Connection
    s))
           let cmd = Builder -> YicesCommand
    safeCmd Builder
    "(show-unsat-core)"
           case mb of
             Right (SExp -> Maybe [Text]
    asAtomList -> Just [Text]
    nms) -> [Text] -> IO [Text]
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return [Text]
    nms

             Right (SApp [SAtom Text
    "error", SString Text
    msg]) -> YicesException -> IO [Text]
    forall a e. (?callStack::CallStack, Exception e) => e -> a
    throw (YicesCommand -> Text -> YicesException
    YicesError YicesCommand
    cmd Text
    msg)
             Right SExp
    res -> YicesException -> IO [Text]
    forall a e. (?callStack::CallStack, Exception e) => e -> a
    throw (YicesCommand -> Text -> YicesException
    YicesParseError YicesCommand
    cmd ([Char] -> Text
    Text.pack (SExp -> [Char]
    forall a. Show a => a -> [Char]
    show SExp
    res)))
             Left (SomeException e
    e) -> YicesException -> IO [Text]
    forall a e. (?callStack::CallStack, Exception e) => e -> a
    throw (YicesException -> IO [Text]) -> YicesException -> IO [Text]
    forall a b. (a -> b) -> a -> b
    $ YicesCommand -> Text -> YicesException
    YicesParseError YicesCommand
    cmd (Text -> YicesException) -> Text -> YicesException
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Text
    Text.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $
                     [[Char]] -> [Char]
    unlines [ [Char]
    "Could not parse unsat core result."
                             , [Char]
    "*** Exception: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ e -> [Char]
    forall e. Exception e => e -> [Char]
    displayException e
    e
                             ]
      smtAbductResult :: forall (f :: Type -> Type) t.
    f Connection
    -> WriterConn t Connection -> Text -> Term Connection -> IO [Char]
    smtAbductResult f Connection
    _ WriterConn t Connection
    _ Text
    _ = [Char] -> YicesTerm -> IO [Char]
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "abduction"

      smtAbductNextResult :: forall (f :: Type -> Type) t.
    f Connection -> WriterConn t Connection -> IO [Char]
    smtAbductNextResult f Connection
    _ = [Char] -> WriterConn t Connection -> IO [Char]
    forall a. [Char] -> a
    unsupportedFeature [Char]
    "abduction"

    -- | Exceptions that can occur when reading responses from Yices
    data YicesException
      = YicesUnsupported YicesCommand
      | YicesError YicesCommand Text
      | YicesParseError YicesCommand Text

    instance Show YicesException where
      show :: YicesException -> [Char]
    show (YicesUnsupported (YicesCommand Bool
    _ Builder
    cmd)) =
         [[Char]] -> [Char]
    unlines
           [ [Char]
    "unsupported command:"
           , [Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ LazyText -> [Char]
    Lazy.unpack (Builder -> LazyText
    Builder.toLazyText Builder
    cmd)
           ]
      show (YicesError (YicesCommand Bool
    _ Builder
    cmd) Text
    msg) =
         [[Char]] -> [Char]
    unlines
           [ [Char]
    "Solver reported an error:"
           , [Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Text -> [Char]
    Text.unpack Text
    msg
           , [Char]
    "in response to command:"
           , [Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ LazyText -> [Char]
    Lazy.unpack (Builder -> LazyText
    Builder.toLazyText Builder
    cmd)
           ]
      show (YicesParseError (YicesCommand Bool
    _ Builder
    cmd) Text
    msg) =
         [[Char]] -> [Char]
    unlines
           [ [Char]
    "Could not parse solver response:"
           , [Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Text -> [Char]
    Text.unpack Text
    msg
           , [Char]
    "in response to command:"
           , [Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ LazyText -> [Char]
    Lazy.unpack (Builder -> LazyText
    Builder.toLazyText Builder
    cmd)
           ]

    instance Exception YicesException

    instance OnlineSolver Connection where
      startSolverProcess :: forall scope (st :: Type -> Type) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope Connection)
    startSolverProcess = ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope Connection)
    forall scope (st :: Type -> Type) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope Connection)
    yicesStartSolver
      shutdownSolverProcess :: forall scope.
    SolverProcess scope Connection -> IO (ExitCode, LazyText)
    shutdownSolverProcess = SolverProcess scope Connection -> IO (ExitCode, LazyText)
    forall scope.
    SolverProcess scope Connection -> IO (ExitCode, LazyText)
    yicesShutdownSolver

    yicesShutdownSolver :: SolverProcess s Connection -> IO (ExitCode, Lazy.Text)
    yicesShutdownSolver :: forall scope.
    SolverProcess scope Connection -> IO (ExitCode, LazyText)
    yicesShutdownSolver SolverProcess s Connection
    p =
       do WriterConn s Connection -> Command Connection -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommandNoAck (SolverProcess s Connection -> WriterConn s Connection
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess s Connection
    p) Command Connection
    exitCommand
          Maybe Text -> OutputStream Text -> IO ()
    forall a. Maybe a -> OutputStream a -> IO ()
    Streams.write Maybe Text
    forall a. Maybe a
    Nothing (SolverProcess s Connection -> OutputStream Text
    forall t solver. SolverProcess t solver -> OutputStream Text
    solverStdin SolverProcess s Connection
    p)

          --logLn 2 "Waiting for yices to terminate"
          txt <- HandleReader -> IO LazyText
    readAllLines (SolverProcess s Connection -> HandleReader
    forall scope solver. SolverProcess scope solver -> HandleReader
    solverStderr SolverProcess s Connection
    p)
          stopHandleReader (solverStderr p)

          ec <- solverCleanupCallback p
          return (ec,txt)

    yicesAck ::
      IORef (Maybe Int) ->
      AcknowledgementAction s Connection
    yicesAck :: forall s. IORef (Maybe Int) -> AcknowledgementAction s Connection
    yicesAck IORef (Maybe Int)
    earlyUnsatRef = (WriterConn s Connection -> Command Connection -> IO ())
    -> AcknowledgementAction s Connection
    forall t h.
    (WriterConn t h -> Command h -> IO ()) -> AcknowledgementAction t h
    AckAction ((WriterConn s Connection -> Command Connection -> IO ())
     -> AcknowledgementAction s Connection)
    -> (WriterConn s Connection -> Command Connection -> IO ())
    -> AcknowledgementAction s Connection
    forall a b. (a -> b) -> a -> b
    $ \WriterConn s Connection
    conn Command Connection
    cmdf ->
      do isEarlyUnsat <- IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef IORef (Maybe Int)
    earlyUnsatRef
         let cmd = Command Connection
    Connection -> YicesCommand
    cmdf (WriterConn s Connection -> Connection
    forall t h. WriterConn t h -> h
    connState WriterConn s Connection
    conn)
             earlyUnsatSafe = YicesCommand -> Bool
    cmdEarlyUnsatSafe YicesCommand
    cmd
             cmdBuilder = YicesCommand -> Builder
    cmdCmd YicesCommand
    cmd
         if isJust isEarlyUnsat && not earlyUnsatSafe
         then return ()
         else do
           x <- getAckResponse (connInputHandle conn)
           case x of
             Maybe Text
    Nothing ->
               () -> IO ()
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
             Just Text
    "unsat" ->
               do i <- WriterConn s Connection -> IO Int
    forall t h. WriterConn t h -> IO Int
    entryStackHeight WriterConn s Connection
    conn
                  writeIORef earlyUnsatRef $! (Just $! if i > 0 then 1 else 0)
             Just Text
    txt ->
               [Char] -> IO ()
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
                       [ [Char]
    "Unexpected response from solver while awaiting acknowledgement"
                       , [Char]
    "*** result:" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Text -> [Char]
    forall a. Show a => a -> [Char]
    show Text
    txt
                       , [Char]
    "in response to command"
                       , [Char]
    "***: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ LazyText -> [Char]
    Lazy.unpack (Builder -> LazyText
    Builder.toLazyText Builder
    cmdBuilder)
                       ]

    yicesStartSolver ::
      ProblemFeatures ->
      Maybe Handle ->
      B.ExprBuilder t st fs ->
      IO (SolverProcess t Connection)
    yicesStartSolver :: forall scope (st :: Type -> Type) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope Connection)
    yicesStartSolver ProblemFeatures
    features Maybe Handle
    auxOutput ExprBuilder t st fs
    sym = do -- FIXME
      let cfg :: Config
    cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
      yices_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
    findSolverPath ConfigOption (BaseStringType Unicode)
    yicesPath Config
    cfg
      enableMCSat <- getOpt =<< getOptionSetting yicesEnableMCSat cfg
      enableInteractive <- getOpt =<< getOptionSetting yicesEnableInteractive cfg
      goalTimeout <- SolverGoalTimeout . (1000*) <$> (getOpt =<< getOptionSetting yicesGoalTimeout cfg)
      let modeFlag | Bool
    enableInteractive
                     Bool -> Bool -> Bool
    || (SolverGoalTimeout -> Integer
    getGoalTimeoutInSeconds SolverGoalTimeout
    goalTimeout) Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0 = [Char]
    "--mode=interactive"
                   | Bool
    otherwise = [Char]
    "--mode=push-pop"
          args = [Char]
    modeFlag [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [Char]
    "--print-success" [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :
                 if Bool
    enableMCSat then [[Char]
    "--mcsat"] else []
          hasNamedAssumptions = ProblemFeatures
    features ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useUnsatCores Bool -> Bool -> Bool
    ||
                                ProblemFeatures
    features ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useUnsatAssumptions
      when (enableMCSat && hasNamedAssumptions) $
         fail "Unsat cores and named assumptions are incompatible with MC-SAT in Yices."
      let  features' | Bool
    enableMCSat = ProblemFeatures
    features ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useNonlinearArithmetic
                     | Bool
    otherwise = ProblemFeatures
    features

      hdls@(in_h,out_h,err_h,ph) <- startProcess yices_path args Nothing

      (in_stream, out_stream, err_reader) <-
        demuxProcessHandles in_h out_h err_h
          (fmap (\Handle
    x -> (Text
    "; ", Handle
    x)) auxOutput)

      in_stream' <- Streams.atEndOfOutput (hClose in_h) in_stream

      conn <- newConnection in_stream' out_stream yicesAck features' goalTimeout B.emptySymbolVarBimap

      setYicesParams conn cfg

      return $! SolverProcess { solverConn   = conn
                              , solverCleanupCallback = cleanupProcess hdls
                              , solverStderr = err_reader
                              , solverHandle = ph
                              , solverErrorBehavior = ContinueOnError
                              , solverEvalFuns = smtEvalFuns conn out_stream
                              , solverLogFn = logSolverEvent sym
                              , solverName = "Yices"
                              , solverEarlyUnsat = yicesEarlyUnsat (connState conn)
                              , solverSupportsResetAssertions = True
                              , solverGoalTimeout = goalTimeout
                              }

    ------------------------------------------------------------------------
    -- Translation code

    -- | Send a check command to Yices.
    sendCheck :: WriterConn t Connection -> IO ()
    sendCheck :: forall t. WriterConn t Connection -> IO ()
    sendCheck WriterConn t Connection
    c = WriterConn t Connection -> [Command Connection] -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
    addCommands WriterConn t Connection
    c (WriterConn t Connection -> [Command Connection]
    forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
    forall (f :: Type -> Type). f Connection -> [Command Connection]
    checkCommands WriterConn t Connection
    c)

    sendCheckExistsForall :: WriterConn t Connection -> IO ()
    sendCheckExistsForall :: forall t. WriterConn t Connection -> IO ()
    sendCheckExistsForall WriterConn t Connection
    c = WriterConn t Connection -> Command Connection -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommandNoAck WriterConn t Connection
    c Command Connection
    checkExistsForallCommand

    assertForall :: WriterConn t Connection -> [(Text, YicesType)] -> Expr -> IO ()
    assertForall :: forall t.
    WriterConn t Connection
    -> [(Text, YicesType)] -> YicesTerm -> IO ()
    assertForall WriterConn t Connection
    c [(Text, YicesType)]
    vars YicesTerm
    e = WriterConn t Connection -> Command Connection -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn t Connection
    c ([(Text, YicesType)] -> YicesTerm -> Command Connection
    assertForallCommand [(Text, YicesType)]
    vars YicesTerm
    e)

    setParam :: WriterConn t Connection -> ConfigValue -> IO ()
    setParam :: forall t. WriterConn t Connection -> ConfigValue -> IO ()
    setParam WriterConn t Connection
    c (ConfigValue ConfigOption tp
    o ConcreteVal tp
    val) =
      case ConfigOption tp -> [Text]
    forall (tp :: BaseType). ConfigOption tp -> [Text]
    configOptionNameParts ConfigOption tp
    o of
        [Text
    yicesName, Text
    nm] | Text
    yicesName Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    "yices" ->
          case ConcreteVal tp -> Maybe Builder
    forall (tp :: BaseType). ConcreteVal tp -> Maybe Builder
    asYicesConfigValue ConcreteVal tp
    val of
            Just Builder
    v ->
              WriterConn t Connection -> Command Connection -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn t Connection
    c (Text -> Builder -> Command Connection
    setParamCommand Text
    nm Builder
    v)
            Maybe Builder
    Nothing ->
              [Char] -> IO ()
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unwords [[Char]
    "Unknown Yices parameter type:", Text -> [Char]
    forall a. Show a => a -> [Char]
    show Text
    nm]
        [Text]
    _ -> [Char] -> IO ()
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unwords [[Char]
    "not a Yices parameter", ConfigOption tp -> [Char]
    forall (tp :: BaseType). ConfigOption tp -> [Char]
    configOptionName ConfigOption tp
    o]

    setYicesParams :: WriterConn t Connection -> Config -> IO ()
    setYicesParams :: forall t. WriterConn t Connection -> Config -> IO ()
    setYicesParams WriterConn t Connection
    conn Config
    cfg = do
       params <- Text -> Config -> IO [ConfigValue]
    getConfigValues Text
    "yices" Config
    cfg
       forM_ params $ setParam conn

    eval :: WriterConn t Connection -> Term Connection -> IO ()
    eval :: forall t. WriterConn t Connection -> Term Connection -> IO ()
    eval WriterConn t Connection
    c Term Connection
    e = WriterConn t Connection -> Command Connection -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommandNoAck WriterConn t Connection
    c (Term Connection -> Command Connection
    evalCommand Term Connection
    e)

    -- | Print a command to show the model.
    sendShowModel :: WriterConn t Connection -> IO ()
    sendShowModel :: forall t. WriterConn t Connection -> IO ()
    sendShowModel WriterConn t Connection
    c = WriterConn t Connection -> Command Connection -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommandNoAck WriterConn t Connection
    c Command Connection
    showModelCommand

    getAckResponse :: Streams.InputStream Text -> IO (Maybe Text)
    getAckResponse :: InputStream Text -> IO (Maybe Text)
    getAckResponse InputStream Text
    resps =
      do mb <- (SomeException -> Maybe SomeException)
    -> IO SExp -> IO (Either SomeException SExp)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (Parser SExp -> InputStream Text -> IO SExp
    forall r. Parser r -> InputStream Text -> IO r
    Streams.parseFromStream (Parser Text -> Parser SExp
    parseSExp Parser Text
    parseYicesString) InputStream Text
    resps)
         case mb of
           Right (SAtom Text
    "ok") -> Maybe Text -> IO (Maybe Text)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe Text
    forall a. Maybe a
    Nothing
           Right (SAtom Text
    txt)  -> Maybe Text -> IO (Maybe Text)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Text -> Maybe Text
    forall a. a -> Maybe a
    Just Text
    txt)
           Right SExp
    res -> [Char] -> IO (Maybe Text)
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO (Maybe Text)) -> [Char] -> IO (Maybe Text)
    forall a b. (a -> b) -> a -> b
    $
                   [[Char]] -> [Char]
    unlines [ [Char]
    "Could not parse acknowledgement result."
                           , [Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ SExp -> [Char]
    forall a. Show a => a -> [Char]
    show SExp
    res
                           ]
           Left (SomeException e
    e) -> [Char] -> IO (Maybe Text)
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO (Maybe Text)) -> [Char] -> IO (Maybe Text)
    forall a b. (a -> b) -> a -> b
    $
                   [[Char]] -> [Char]
    unlines [ [Char]
    "Could not parse acknowledgement result."
                           , [Char]
    "*** Exception: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ e -> [Char]
    forall e. Exception e => e -> [Char]
    displayException e
    e
                           ]

    -- | Get the sat result from a previous SAT command.
    -- Throws an exception if something goes wrong.
    getSatResponse :: WriterConn t Connection -> IO (SatResult () ())
    getSatResponse :: forall t. WriterConn t Connection -> IO (SatResult () ())
    getSatResponse WriterConn t Connection
    conn =
      let interpretSExpr :: SExp -> SatResult () ()
    interpretSExpr = \case
            (SAtom Text
    "unsat")   -> () -> SatResult () ()
    forall mdl core. core -> SatResult mdl core
    Unsat ()
            (SAtom Text
    "sat")     -> () -> SatResult () ()
    forall mdl core. mdl -> SatResult mdl core
    Sat ()
            (SAtom Text
    "unknown") -> SatResult () ()
    forall mdl core. SatResult mdl core
    Unknown
            (SAtom Text
    "interrupted") -> SatResult () ()
    forall mdl core. SatResult mdl core
    Unknown
            SExp
    res -> UnparseableYicesResponse -> SatResult () ()
    forall a e. (?callStack::CallStack, Exception e) => e -> a
    throw (UnparseableYicesResponse -> SatResult () ())
    -> UnparseableYicesResponse -> SatResult () ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> UnparseableYicesResponse
    UnparseableYicesResponse ([Char] -> UnparseableYicesResponse)
    -> [Char] -> UnparseableYicesResponse
    forall a b. (a -> b) -> a -> b
    $
                   [[Char]] -> [Char]
    unlines [ [Char]
    "Could not parse sat result."
                           , [Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ SExp -> [Char]
    forall a. Show a => a -> [Char]
    show SExp
    res
                           ]
          tmo :: Integer
    tmo = SolverGoalTimeout -> Integer
    getGoalTimeoutInSeconds (SolverGoalTimeout -> Integer) -> SolverGoalTimeout -> Integer
    forall a b. (a -> b) -> a -> b
    $ Connection -> SolverGoalTimeout
    yicesTimeout (Connection -> SolverGoalTimeout)
    -> Connection -> SolverGoalTimeout
    forall a b. (a -> b) -> a -> b
    $ WriterConn t Connection -> Connection
    forall t h. WriterConn t h -> h
    connState WriterConn t Connection
    conn
          delay :: Integer
    delay = Integer
    500  -- allow solver to honor timeout first
          msec2usec :: Int -> Int
    msec2usec = (Int
    1000 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *)
          deadman_tmo :: Int
    deadman_tmo = Int -> Int
    msec2usec (Int -> Int) -> Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    tmo Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    delay)
          deadmanTimer :: IO ()
    deadmanTimer = Int -> IO ()
    threadDelay Int
    deadman_tmo
          action :: InputStream Text -> IO SExp
    action = Parser SExp -> InputStream Text -> IO SExp
    forall r. Parser r -> InputStream Text -> IO r
    Streams.parseFromStream (Parser Text -> Parser SExp
    parseSExp Parser Text
    parseYicesString)
      in if Integer
    tmo Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0
         then (SomeException -> Maybe SomeException)
    -> IO SExp -> IO (Either SomeException SExp)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (InputStream Text -> IO SExp
    action (WriterConn t Connection -> InputStream Text
    forall t h. WriterConn t h -> InputStream Text
    connInputHandle WriterConn t Connection
    conn)) IO (Either SomeException SExp)
    -> (Either SomeException SExp -> IO (SatResult () ()))
    -> IO (SatResult () ())
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                Right SExp
    d -> SatResult () () -> IO (SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (SatResult () () -> IO (SatResult () ()))
    -> SatResult () () -> IO (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $ SExp -> SatResult () ()
    interpretSExpr SExp
    d
                Left SomeException
    e -> [Char] -> IO (SatResult () ())
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO (SatResult () ())) -> [Char] -> IO (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [ [Char]
    "Could not parse sat result."
                                         , [Char]
    "*** Exception: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ SomeException -> [Char]
    forall e. Exception e => e -> [Char]
    displayException SomeException
    e
                                         ]
         else IO ()
    -> IO (Either SomeException SExp)
    -> IO (Either () (Either SomeException SExp))
    forall a b. IO a -> IO b -> IO (Either a b)
    race IO ()
    deadmanTimer ((SomeException -> Maybe SomeException)
    -> IO SExp -> IO (Either SomeException SExp)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (IO SExp -> IO (Either SomeException SExp))
    -> IO SExp -> IO (Either SomeException SExp)
    forall a b. (a -> b) -> a -> b
    $ InputStream Text -> IO SExp
    action (WriterConn t Connection -> InputStream Text
    forall t h. WriterConn t h -> InputStream Text
    connInputHandle WriterConn t Connection
    conn)) IO (Either () (Either SomeException SExp))
    -> (Either () (Either SomeException SExp) -> IO (SatResult () ()))
    -> IO (SatResult () ())
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Right (Right SExp
    x) -> SatResult () () -> IO (SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (SatResult () () -> IO (SatResult () ()))
    -> SatResult () () -> IO (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $ SExp -> SatResult () ()
    interpretSExpr SExp
    x
              Left () -> SatResult () () -> IO (SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SatResult () ()
    forall mdl core. SatResult mdl core
    Unknown  -- no response in timeout period
              Right (Left SomeException
    e) -> [Char] -> IO (SatResult () ())
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO (SatResult () ())) -> [Char] -> IO (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [ [Char]
    "Could not parse sat result."
                                               , [Char]
    "*** Exception: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ SomeException -> [Char]
    forall e. Exception e => e -> [Char]
    displayException SomeException
    e
                                               ]

    data UnparseableYicesResponse = UnparseableYicesResponse String deriving Int -> UnparseableYicesResponse -> [Char] -> [Char]
    [UnparseableYicesResponse] -> [Char] -> [Char]
    UnparseableYicesResponse -> [Char]
    (Int -> UnparseableYicesResponse -> [Char] -> [Char])
    -> (UnparseableYicesResponse -> [Char])
    -> ([UnparseableYicesResponse] -> [Char] -> [Char])
    -> Show UnparseableYicesResponse
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> UnparseableYicesResponse -> [Char] -> [Char]
    showsPrec :: Int -> UnparseableYicesResponse -> [Char] -> [Char]
    $cshow :: UnparseableYicesResponse -> [Char]
    show :: UnparseableYicesResponse -> [Char]
    $cshowList :: [UnparseableYicesResponse] -> [Char] -> [Char]
    showList :: [UnparseableYicesResponse] -> [Char] -> [Char]
    Show
    instance Exception UnparseableYicesResponse

    type Eval scope ty =
      WriterConn scope Connection ->
      Streams.InputStream Text ->
      Term Connection ->
      IO ty

    -- | Call eval to get a Rational term
    yicesEvalReal :: Eval s Rational
    yicesEvalReal :: forall s. Eval s Rational
    yicesEvalReal WriterConn s Connection
    conn InputStream Text
    resp Term Connection
    tm =
      do WriterConn s Connection -> Term Connection -> IO ()
    forall t. WriterConn t Connection -> Term Connection -> IO ()
    eval WriterConn s Connection
    conn Term Connection
    tm
         mb <- (SomeException -> Maybe SomeException)
    -> IO (Root Rational) -> IO (Either SomeException (Root Rational))
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (Parser (Root Rational) -> InputStream Text -> IO (Root Rational)
    forall r. Parser r -> InputStream Text -> IO r
    Streams.parseFromStream (Parser ()
    skipSpaceOrNewline Parser () -> Parser (Root Rational) -> Parser (Root Rational)
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser (Root Rational)
    Root.parseYicesRoot) InputStream Text
    resp)
         case mb of
           Left (SomeException e
    ex) ->
               [Char] -> IO Rational
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO Rational) -> [Char] -> IO Rational
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
                 [ [Char]
    "Could not parse real value returned by yices: "
                 , e -> [Char]
    forall e. Exception e => e -> [Char]
    displayException e
    ex
                 ]
           Right Root Rational
    r -> Rational -> IO Rational
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Rational -> IO Rational) -> Rational -> IO Rational
    forall a b. (a -> b) -> a -> b
    $ Root Rational -> Rational
    Root.approximate Root Rational
    r

    parseYicesString :: Atto.Parser Text
    parseYicesString :: Parser Text
    parseYicesString = Char -> Parser Char
    Atto.char Char
    '\"' Parser Char -> Parser Text -> Parser Text
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Parser Text
    go
     where
     isStringChar :: Char -> Bool
    isStringChar Char
    '\"' = Bool
    False
     isStringChar Char
    '\\' = Bool
    False
     isStringChar Char
    '\n' = Bool
    False
     isStringChar Char
    _    = Bool
    True

     octalDigit :: Parser Char
    octalDigit = (Char -> Bool) -> Parser Char
    Atto.satisfy ([Char] -> Char -> Bool
    Atto.inClass [Char]
    "01234567")

     octalEscape :: Parser Text
    octalEscape =
       do ds <- [Parser Text [Char]] -> Parser Text [Char]
    forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
    Atto.choice [ Int -> Parser Char -> Parser Text [Char]
    forall (m :: Type -> Type) a. Monad m => Int -> m a -> m [a]
    Atto.count Int
    i Parser Char
    octalDigit | Int
    i <- [ Int
    3, Int
    2, Int
    1] ]
          case readOct ds of
            (Int
    c,[Char]
    ""):[(Int, [Char])]
    _ -> Text -> Parser Text
    forall a. a -> Parser Text a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Char -> Text
    Text.singleton (Int -> Char
    forall a. Enum a => Int -> a
    toEnum Int
    c))
            [(Int, [Char])]
    _ -> Parser Text
    forall a. Parser Text a
    forall (m :: Type -> Type) a. MonadPlus m => m a
    mzero

     escape :: Parser Text
    escape = [Parser Text] -> Parser Text
    forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
    Atto.choice
       [ Parser Text
    octalEscape
       , Char -> Parser Char
    Atto.char Char
    'n' Parser Char -> Parser Text -> Parser Text
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Text -> Parser Text
    forall a. a -> Parser Text a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Text
    "\n"
       , Char -> Parser Char
    Atto.char Char
    't' Parser Char -> Parser Text -> Parser Text
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Text -> Parser Text
    forall a. a -> Parser Text a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Text
    "\t"
       , Char -> Text
    Text.singleton (Char -> Text) -> Parser Char -> Parser Text
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Char
    Atto.anyChar
       ]

     go :: Parser Text
    go = do xs <- (Char -> Bool) -> Parser Text
    Atto.takeWhile Char -> Bool
    isStringChar
             (Atto.char '\"' >> return xs)
              <|> (do _ <- Atto.char '\\'
                      e <- escape
                      ys <- go
                      return (xs <> e <> ys))

    boolValue :: Atto.Parser Bool
    boolValue :: Parser Bool
    boolValue =
      [Parser Bool] -> Parser Bool
    forall (t :: Type -> Type) (m :: Type -> Type) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum
      [ Text -> Parser Text
    Atto.string Text
    "true" Parser Text -> Parser Bool -> Parser Bool
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Bool -> Parser Bool
    forall a. a -> Parser Text a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    True
      , Text -> Parser Text
    Atto.string Text
    "false" Parser Text -> Parser Bool -> Parser Bool
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Bool -> Parser Bool
    forall a. a -> Parser Text a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    False
      ]

    -- | Call eval to get a Boolean term.
    yicesEvalBool :: Eval s Bool
    yicesEvalBool :: forall s. Eval s Bool
    yicesEvalBool WriterConn s Connection
    conn InputStream Text
    resp Term Connection
    tm =
      do WriterConn s Connection -> Term Connection -> IO ()
    forall t. WriterConn t Connection -> Term Connection -> IO ()
    eval WriterConn s Connection
    conn Term Connection
    tm
         mb <- (SomeException -> Maybe SomeException)
    -> IO Bool -> IO (Either SomeException Bool)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (Parser Bool -> InputStream Text -> IO Bool
    forall r. Parser r -> InputStream Text -> IO r
    Streams.parseFromStream (Parser ()
    skipSpaceOrNewline Parser () -> Parser Bool -> Parser Bool
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser Bool
    boolValue) InputStream Text
    resp)
         case mb of
           Left (SomeException e
    ex) ->
               [Char] -> IO Bool
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO Bool) -> [Char] -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
                 [ [Char]
    "Could not parse boolean value returned by yices: "
                 , e -> [Char]
    forall e. Exception e => e -> [Char]
    displayException e
    ex
                 ]
           Right Bool
    b -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    b

    yicesBV :: Int -> Atto.Parser Integer
    yicesBV :: Int -> Parser Integer
    yicesBV Int
    w =
      do _ <- Text -> Parser Text
    Atto.string Text
    "0b"
         digits <- Atto.takeWhile (`elem` ("01"::String))
         readBit w (Text.unpack digits)

    -- | Send eval command and get result back.
    yicesEvalBV :: NatRepr w -> Eval s (BV.BV w)
    yicesEvalBV :: forall (w :: Nat) s. NatRepr w -> Eval s (BV w)
    yicesEvalBV NatRepr w
    w WriterConn s Connection
    conn InputStream Text
    resp Term Connection
    tm =
      do WriterConn s Connection -> Term Connection -> IO ()
    forall t. WriterConn t Connection -> Term Connection -> IO ()
    eval WriterConn s Connection
    conn Term Connection
    tm
         mb <- (SomeException -> Maybe SomeException)
    -> IO Integer -> IO (Either SomeException Integer)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (Parser Integer -> InputStream Text -> IO Integer
    forall r. Parser r -> InputStream Text -> IO r
    Streams.parseFromStream (Parser ()
    skipSpaceOrNewline Parser () -> Parser Integer -> Parser Integer
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Int -> Parser Integer
    yicesBV (NatRepr w -> Int
    forall (n :: Nat). NatRepr n -> Int
    widthVal NatRepr w
    w)) InputStream Text
    resp)
         case mb of
           Left (SomeException e
    ex) ->
               [Char] -> IO (BV w)
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO (BV w)) -> [Char] -> IO (BV w)
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
                 [ [Char]
    "Could not parse bitvector value returned by yices: "
                 , e -> [Char]
    forall e. Exception e => e -> [Char]
    displayException e
    ex
                 ]
           Right Integer
    b -> BV w -> IO (BV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (NatRepr w -> Integer -> BV w
    forall (w :: Nat). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w Integer
    b)

    readBit :: MonadFail m => Int -> String -> m Integer
    readBit :: forall (m :: Type -> Type).
    MonadFail m =>
    Int -> [Char] -> m Integer
    readBit Int
    w0 = Int -> Integer -> [Char] -> m Integer
    go Int
    0 Integer
    0
      where go :: Int -> Integer -> [Char] -> m Integer
    go Int
    n Integer
    v [Char]
    "" = do
              Bool -> m () -> m ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    w0) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> m ()
    forall a. [Char] -> m a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail [Char]
    "Value has a different number of bits than we expected."
              Integer -> m Integer
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Integer
    v
            go Int
    n Integer
    v (Char
    c:[Char]
    r) = do
              case Char
    c of
                Char
    '0' -> Int -> Integer -> [Char] -> m Integer
    go (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) (Integer
    v Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    1)       [Char]
    r
                Char
    '1' -> Int -> Integer -> [Char] -> m Integer
    go (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) ((Integer
    v Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    1) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) [Char]
    r
                Char
    _ -> [Char] -> m Integer
    forall a. [Char] -> m a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail [Char]
    "Not a bitvector."

    ------------------------------------------------------------------
    -- SolverAdapter interface

    yicesSMT2Features :: ProblemFeatures
    yicesSMT2Features :: ProblemFeatures
    yicesSMT2Features
      =   ProblemFeatures
    useComputableReals
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useIntegerArithmetic
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useBitvectors
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useQuantifiers

    yicesDefaultFeatures :: ProblemFeatures
    yicesDefaultFeatures :: ProblemFeatures
    yicesDefaultFeatures
        = ProblemFeatures
    useIntegerArithmetic
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useBitvectors
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useStructs

    yicesAdapter :: SolverAdapter t
    yicesAdapter :: forall (t :: Type -> Type). SolverAdapter t
    yicesAdapter =
       SolverAdapter
       { solver_adapter_name :: [Char]
    solver_adapter_name = [Char]
    "yices"
       , solver_adapter_config_options :: [ConfigDesc]
    solver_adapter_config_options = [ConfigDesc]
    yicesOptions
       , solver_adapter_check_sat :: forall t fs a.
    ExprBuilder t t fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    solver_adapter_check_sat = \ExprBuilder t t fs
    sym LogData
    logData [BoolExpr t]
    ps SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
    cont ->
           ExprBuilder t t fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t) () -> IO a)
    -> IO a
    forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t) () -> IO a)
    -> IO a
    runYicesInOverride ExprBuilder t t fs
    sym LogData
    logData [BoolExpr t]
    ps
              (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
    cont (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
     -> IO a)
    -> (SatResult (GroundEvalFn t) ()
        -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ())
    -> SatResult (GroundEvalFn t) ()
    -> IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Identity
      (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ())
    -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    forall a. Identity a -> a
    runIdentity (Identity
       (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ())
     -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ())
    -> (SatResult (GroundEvalFn t) ()
        -> Identity
             (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()))
    -> SatResult (GroundEvalFn t) ()
    -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (GroundEvalFn t
     -> Identity (GroundEvalFn t, Maybe (ExprRangeBindings t)))
    -> (() -> Identity ())
    -> SatResult (GroundEvalFn t) ()
    -> Identity
         (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ())
    forall (t :: Type -> Type) a q b r.
    Applicative t =>
    (a -> t q) -> (b -> t r) -> SatResult a b -> t (SatResult q r)
    traverseSatResult (\GroundEvalFn t
    x -> (GroundEvalFn t, Maybe (ExprRangeBindings t))
    -> Identity (GroundEvalFn t, Maybe (ExprRangeBindings t))
    forall a. a -> Identity a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (GroundEvalFn t
    x,Maybe (ExprRangeBindings t)
    forall a. Maybe a
    Nothing)) () -> Identity ()
    forall a. a -> Identity a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure)
       , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t t fs -> Handle -> [BoolExpr t] -> IO ()
    solver_adapter_write_smt2 =
           ()
    -> [Char]
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t t fs
    -> Handle
    -> [BoolExpr t]
    -> IO ()
    forall a t (st :: Type -> Type) fs.
    SMTLib2Tweaks a =>
    a
    -> [Char]
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> Handle
    -> [BoolExpr t]
    -> IO ()
    writeDefaultSMT2 () [Char]
    "YICES" ProblemFeatures
    yicesSMT2Features (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    yicesStrictParsing)
       }

    -- | Path to yices
    yicesPath :: ConfigOption (BaseStringType Unicode)
    yicesPath :: ConfigOption (BaseStringType Unicode)
    yicesPath = BaseTypeRepr (BaseStringType Unicode)
    -> [Char] -> ConfigOption (BaseStringType Unicode)
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr (BaseStringType Unicode)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "solver.yices.path"

    yicesPathOLD :: ConfigOption (BaseStringType Unicode)
    yicesPathOLD :: ConfigOption (BaseStringType Unicode)
    yicesPathOLD = BaseTypeRepr (BaseStringType Unicode)
    -> [Char] -> ConfigOption (BaseStringType Unicode)
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr (BaseStringType Unicode)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "yices_path"

    -- | Enable the MC-SAT solver
    yicesEnableMCSat :: ConfigOption BaseBoolType
    yicesEnableMCSat :: ConfigOption BaseBoolType
    yicesEnableMCSat = BaseTypeRepr BaseBoolType -> [Char] -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseBoolType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "solver.yices.enable-mcsat"

    yicesEnableMCSatOLD :: ConfigOption BaseBoolType
    yicesEnableMCSatOLD :: ConfigOption BaseBoolType
    yicesEnableMCSatOLD = BaseTypeRepr BaseBoolType -> [Char] -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseBoolType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "yices_enable-mcsat"

    -- | Enable interactive mode (necessary for per-goal timeouts)
    yicesEnableInteractive :: ConfigOption BaseBoolType
    yicesEnableInteractive :: ConfigOption BaseBoolType
    yicesEnableInteractive = BaseTypeRepr BaseBoolType -> [Char] -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseBoolType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "solver.yices.enable-interactive"

    yicesEnableInteractiveOLD :: ConfigOption BaseBoolType
    yicesEnableInteractiveOLD :: ConfigOption BaseBoolType
    yicesEnableInteractiveOLD = BaseTypeRepr BaseBoolType -> [Char] -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseBoolType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "yices_enable-interactive"

    -- | Set a per-goal timeout in seconds.
    yicesGoalTimeout :: ConfigOption BaseIntegerType
    yicesGoalTimeout :: ConfigOption BaseIntegerType
    yicesGoalTimeout = BaseTypeRepr BaseIntegerType
    -> [Char] -> ConfigOption BaseIntegerType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseIntegerType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "solver.yices.goal-timeout"

    yicesGoalTimeoutOLD :: ConfigOption BaseIntegerType
    yicesGoalTimeoutOLD :: ConfigOption BaseIntegerType
    yicesGoalTimeoutOLD = BaseTypeRepr BaseIntegerType
    -> [Char] -> ConfigOption BaseIntegerType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseIntegerType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "yices_goal-timeout"

    -- | Control strict parsing for Yices solver responses (defaults
    -- to solver.strict-parsing option setting).
    yicesStrictParsing :: ConfigOption BaseBoolType
    yicesStrictParsing :: ConfigOption BaseBoolType
    yicesStrictParsing = BaseTypeRepr BaseBoolType -> [Char] -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseBoolType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr [Char]
    "solver.yices.strict_parsing"

    yicesOptions :: [ConfigDesc]
    yicesOptions :: [ConfigDesc]
    yicesOptions =
      let mkPath :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
    mkPath ConfigOption (BaseStringType Unicode)
    co = ConfigOption (BaseStringType Unicode)
    -> OptionStyle (BaseStringType Unicode)
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal (BaseStringType Unicode))
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt ConfigOption (BaseStringType Unicode)
    co
                      OptionStyle (BaseStringType Unicode)
    executablePathOptSty
                      (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just Doc Void
    "Yices executable path")
                      (ConcreteVal (BaseStringType Unicode)
    -> Maybe (ConcreteVal (BaseStringType Unicode))
    forall a. a -> Maybe a
    Just (StringLiteral Unicode -> ConcreteVal (BaseStringType Unicode)
    forall (si :: StringInfo).
    StringLiteral si -> ConcreteVal ('BaseStringType si)
    ConcreteString StringLiteral Unicode
    "yices"))
          mkMCSat :: ConfigOption BaseBoolType -> ConfigDesc
    mkMCSat ConfigOption BaseBoolType
    co = ConfigOption BaseBoolType
    -> OptionStyle BaseBoolType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal BaseBoolType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt ConfigOption BaseBoolType
    co
                       OptionStyle BaseBoolType
    boolOptSty
                       (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just Doc Void
    "Enable the Yices MCSAT solving engine")
                       (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
    forall a. a -> Maybe a
    Just (Bool -> ConcreteVal BaseBoolType
    ConcreteBool Bool
    False))
          mkIntr :: ConfigOption BaseBoolType -> ConfigDesc
    mkIntr ConfigOption BaseBoolType
    co = ConfigOption BaseBoolType
    -> OptionStyle BaseBoolType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal BaseBoolType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt ConfigOption BaseBoolType
    co
                      OptionStyle BaseBoolType
    boolOptSty
                      (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just Doc Void
    "Enable Yices interactive mode (needed to support timeouts)")
                      (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
    forall a. a -> Maybe a
    Just (Bool -> ConcreteVal BaseBoolType
    ConcreteBool Bool
    False))
          mkTmout :: ConfigOption BaseIntegerType -> ConfigDesc
    mkTmout ConfigOption BaseIntegerType
    co = ConfigOption BaseIntegerType
    -> OptionStyle BaseIntegerType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal BaseIntegerType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt ConfigOption BaseIntegerType
    co
                       OptionStyle BaseIntegerType
    integerOptSty
                       (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just Doc Void
    "Set a per-goal timeout")
                       (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
    forall a. a -> Maybe a
    Just (Integer -> ConcreteVal BaseIntegerType
    ConcreteInteger Integer
    0))
          p :: ConfigDesc
    p = ConfigOption (BaseStringType Unicode) -> ConfigDesc
    mkPath ConfigOption (BaseStringType Unicode)
    yicesPath
          m :: ConfigDesc
    m = ConfigOption BaseBoolType -> ConfigDesc
    mkMCSat ConfigOption BaseBoolType
    yicesEnableMCSat
          i :: ConfigDesc
    i = ConfigOption BaseBoolType -> ConfigDesc
    mkIntr ConfigOption BaseBoolType
    yicesEnableInteractive
          t :: ConfigDesc
    t = ConfigOption BaseIntegerType -> ConfigDesc
    mkTmout ConfigOption BaseIntegerType
    yicesGoalTimeout
      in [ ConfigDesc
    p, ConfigDesc
    m, ConfigDesc
    i, ConfigDesc
    t
         , (Text -> Text) -> ConfigDesc -> ConfigDesc
    copyOpt (Text -> Text -> Text
    forall a b. a -> b -> a
    const (Text -> Text -> Text) -> Text -> Text -> Text
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseBoolType -> Text
    forall (tp :: BaseType). ConfigOption tp -> Text
    configOptionText ConfigOption BaseBoolType
    yicesStrictParsing) ConfigDesc
    strictSMTParseOpt
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    p] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption (BaseStringType Unicode) -> ConfigDesc
    mkPath ConfigOption (BaseStringType Unicode)
    yicesPathOLD
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    m] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseBoolType -> ConfigDesc
    mkMCSat ConfigOption BaseBoolType
    yicesEnableMCSatOLD
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    i] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseBoolType -> ConfigDesc
    mkIntr ConfigOption BaseBoolType
    yicesEnableInteractiveOLD
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    t] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseIntegerType -> ConfigDesc
    mkTmout ConfigOption BaseIntegerType
    yicesGoalTimeoutOLD
         ]
         [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
    forall a. [a] -> [a] -> [a]
    ++ [ConfigDesc]
    yicesInternalOptions

    yicesBranchingChoices :: Set Text
    yicesBranchingChoices :: Set Text
    yicesBranchingChoices = [Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Set.fromList
      [ Text
    "default"
      , Text
    "negative"
      , Text
    "positive"
      , Text
    "theory"
      , Text
    "th-pos"
      , Text
    "th-neg"
      ]

    yicesEFGenModes :: Set Text
    yicesEFGenModes :: Set Text
    yicesEFGenModes = [Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Set.fromList
      [ Text
    "auto"
      , Text
    "none"
      , Text
    "substitution"
      , Text
    "projection"
      ]

    booleanOpt :: String -> [ConfigDesc]
    booleanOpt :: [Char] -> [ConfigDesc]
    booleanOpt [Char]
    nm =
      let b :: ConfigDesc
    b = ConfigOption BaseBoolType -> ConfigDesc
    booleanOpt' (BaseTypeRepr BaseBoolType -> [Char] -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseBoolType
    BaseBoolRepr ([Char]
    "solver.yices."[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    nm))
      in [ ConfigDesc
    b
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    b] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseBoolType -> ConfigDesc
    booleanOpt' (BaseTypeRepr BaseBoolType -> [Char] -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseBoolType
    BaseBoolRepr ([Char]
    "yices."[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    nm))
         ]

    booleanOpt' :: ConfigOption BaseBoolType -> ConfigDesc
    booleanOpt' :: ConfigOption BaseBoolType -> ConfigDesc
    booleanOpt' ConfigOption BaseBoolType
    o =
      ConfigOption BaseBoolType
    -> OptionStyle BaseBoolType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal BaseBoolType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt ConfigOption BaseBoolType
    o
            OptionStyle BaseBoolType
    boolOptSty
            Maybe (Doc Void)
    forall a. Maybe a
    Nothing
            Maybe (ConcreteVal BaseBoolType)
    forall a. Maybe a
    Nothing

    floatWithRangeOpt :: String -> Rational -> Rational -> [ConfigDesc]
    floatWithRangeOpt :: [Char] -> Rational -> Rational -> [ConfigDesc]
    floatWithRangeOpt [Char]
    nm Rational
    lo Rational
    hi =
      let mkO :: [Char] -> ConfigDesc
    mkO [Char]
    n = ConfigOption 'BaseRealType
    -> OptionStyle 'BaseRealType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal 'BaseRealType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt (BaseTypeRepr 'BaseRealType -> [Char] -> ConfigOption 'BaseRealType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr 'BaseRealType
    BaseRealRepr ([Char] -> ConfigOption 'BaseRealType)
    -> [Char] -> ConfigOption 'BaseRealType
    forall a b. (a -> b) -> a -> b
    $ [Char]
    n[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    nm)
                  (Bound Rational -> Bound Rational -> OptionStyle 'BaseRealType
    realWithRangeOptSty (Rational -> Bound Rational
    forall r. r -> Bound r
    Inclusive Rational
    lo) (Rational -> Bound Rational
    forall r. r -> Bound r
    Inclusive Rational
    hi))
                  Maybe (Doc Void)
    forall a. Maybe a
    Nothing
                  Maybe (ConcreteVal 'BaseRealType)
    forall a. Maybe a
    Nothing
          f :: ConfigDesc
    f = [Char] -> ConfigDesc
    mkO [Char]
    "solver.yices."
      in [ ConfigDesc
    f
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    f] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> ConfigDesc
    mkO [Char]
    "yices."
         ]

    floatWithMinOpt :: String -> Bound Rational -> [ConfigDesc]
    floatWithMinOpt :: [Char] -> Bound Rational -> [ConfigDesc]
    floatWithMinOpt [Char]
    nm Bound Rational
    lo =
      let mkO :: [Char] -> ConfigDesc
    mkO [Char]
    n = ConfigOption 'BaseRealType
    -> OptionStyle 'BaseRealType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal 'BaseRealType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt (BaseTypeRepr 'BaseRealType -> [Char] -> ConfigOption 'BaseRealType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr 'BaseRealType
    BaseRealRepr ([Char] -> ConfigOption 'BaseRealType)
    -> [Char] -> ConfigOption 'BaseRealType
    forall a b. (a -> b) -> a -> b
    $ [Char]
    n[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    nm)
                  (Bound Rational -> OptionStyle 'BaseRealType
    realWithMinOptSty Bound Rational
    lo)
                  Maybe (Doc Void)
    forall a. Maybe a
    Nothing
                  Maybe (ConcreteVal 'BaseRealType)
    forall a. Maybe a
    Nothing
          f :: ConfigDesc
    f = [Char] -> ConfigDesc
    mkO [Char]
    "solver.yices."
      in [ ConfigDesc
    f
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    f] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> ConfigDesc
    mkO [Char]
    "yices."
         ]

    intWithRangeOpt :: String -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt :: [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt [Char]
    nm Integer
    lo Integer
    hi =
      let mkO :: [Char] -> ConfigDesc
    mkO [Char]
    n = ConfigOption BaseIntegerType
    -> OptionStyle BaseIntegerType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal BaseIntegerType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt (BaseTypeRepr BaseIntegerType
    -> [Char] -> ConfigOption BaseIntegerType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption BaseTypeRepr BaseIntegerType
    BaseIntegerRepr ([Char] -> ConfigOption BaseIntegerType)
    -> [Char] -> ConfigOption BaseIntegerType
    forall a b. (a -> b) -> a -> b
    $ [Char]
    n[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    nm)
                  (Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
    integerWithRangeOptSty (Integer -> Bound Integer
    forall r. r -> Bound r
    Inclusive Integer
    lo) (Integer -> Bound Integer
    forall r. r -> Bound r
    Inclusive Integer
    hi))
                  Maybe (Doc Void)
    forall a. Maybe a
    Nothing
                  Maybe (ConcreteVal BaseIntegerType)
    forall a. Maybe a
    Nothing
          i :: ConfigDesc
    i = [Char] -> ConfigDesc
    mkO [Char]
    "solver.yices."
      in [ ConfigDesc
    i
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    i] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> ConfigDesc
    mkO [Char]
    "yices."
         ]

    enumOpt :: String -> Set Text -> [ConfigDesc]
    enumOpt :: [Char] -> Set Text -> [ConfigDesc]
    enumOpt [Char]
    nm Set Text
    xs =
      let mkO :: [Char] -> ConfigDesc
    mkO [Char]
    n = ConfigOption (BaseStringType Unicode)
    -> OptionStyle (BaseStringType Unicode)
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal (BaseStringType Unicode))
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt (BaseTypeRepr (BaseStringType Unicode)
    -> [Char] -> ConfigOption (BaseStringType Unicode)
    forall (tp :: BaseType).
    BaseTypeRepr tp -> [Char] -> ConfigOption tp
    configOption (StringInfoRepr Unicode -> BaseTypeRepr (BaseStringType Unicode)
    forall (si :: StringInfo).
    StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
    BaseStringRepr StringInfoRepr Unicode
    UnicodeRepr) ([Char] -> ConfigOption (BaseStringType Unicode))
    -> [Char] -> ConfigOption (BaseStringType Unicode)
    forall a b. (a -> b) -> a -> b
    $ [Char]
    n[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    nm)
                  (Set Text -> OptionStyle (BaseStringType Unicode)
    enumOptSty Set Text
    xs)
                  Maybe (Doc Void)
    forall a. Maybe a
    Nothing
                  Maybe (ConcreteVal (BaseStringType Unicode))
    forall a. Maybe a
    Nothing
          e :: ConfigDesc
    e = [Char] -> ConfigDesc
    mkO [Char]
    "solver.yices."
      in [ ConfigDesc
    e
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    e] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> ConfigDesc
    mkO [Char]
    "yices."
         ]

    yicesInternalOptions :: [ConfigDesc]
    yicesInternalOptions :: [ConfigDesc]
    yicesInternalOptions = [[ConfigDesc]] -> [ConfigDesc]
    forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
    concat
      [ [Char] -> [ConfigDesc]
    booleanOpt [Char]
    "var-elim"
      , [Char] -> [ConfigDesc]
    booleanOpt [Char]
    "arith-elim"
      , [Char] -> [ConfigDesc]
    booleanOpt [Char]
    "flatten"
      , [Char] -> [ConfigDesc]
    booleanOpt [Char]
    "learn-eq"
      , [Char] -> [ConfigDesc]
    booleanOpt [Char]
    "keep-ite"
      , [Char] -> [ConfigDesc]
    booleanOpt [Char]
    "fast-restarts"

      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "c-threshold" Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Bound Rational -> [ConfigDesc]
    floatWithMinOpt   [Char]
    "c-factor"    (Rational -> Bound Rational
    forall r. r -> Bound r
    Inclusive Rational
    1)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "d-threshold" Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Rational -> Rational -> [ConfigDesc]
    floatWithRangeOpt [Char]
    "d-factor"    Rational
    1 Rational
    1.5
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "r-threshold" Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Rational -> Rational -> [ConfigDesc]
    floatWithRangeOpt [Char]
    "r-fraction"  Rational
    0 Rational
    1
      , [Char] -> Bound Rational -> [ConfigDesc]
    floatWithMinOpt   [Char]
    "r-factor"    (Rational -> Bound Rational
    forall r. r -> Bound r
    Inclusive Rational
    1)

      , [Char] -> Rational -> Rational -> [ConfigDesc]
    floatWithRangeOpt [Char]
    "var-decay"  Rational
    0 Rational
    1
      , [Char] -> Rational -> Rational -> [ConfigDesc]
    floatWithRangeOpt [Char]
    "randomness" Rational
    0 Rational
    1
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "random-seed" (Integer -> Integer
    forall a. Num a => a -> a
    negate (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)) (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Set Text -> [ConfigDesc]
    enumOpt           [Char]
    "branching"   Set Text
    yicesBranchingChoices
      , [Char] -> Rational -> Rational -> [ConfigDesc]
    floatWithRangeOpt [Char]
    "clause-decay" Rational
    0 Rational
    1
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "cache-tclauses"
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "tclause-size" Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "dyn-ack"
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "dyn-bool-ack"

      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "max-ack"                Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "max-bool-ack"           Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "aux-eq-quota"           Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Bound Rational -> [ConfigDesc]
    floatWithMinOpt   [Char]
    "aux-eq-ratio"           (Rational -> Bound Rational
    forall r. r -> Bound r
    Exclusive Rational
    0)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "dyn-ack-threshold"      Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    16::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "dyn-bool-ack-threshold" Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    16::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "max-interface-eqs"      Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "eager-lemmas"
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "simplex-prop"
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "prop-threshold"         Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "simplex-adjust"
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "bland-threshold"        Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "icheck"
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "icheck-period"          Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "max-update-conflicts"   Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "max-extensionality"     Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "bvarith-elim"
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "optimistic-fcheck"

      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "ef-flatten-iff"
      , [Char] -> [ConfigDesc]
    booleanOpt        [Char]
    "ef-flatten-ite"
      , [Char] -> Set Text -> [ConfigDesc]
    enumOpt           [Char]
    "ef-gen-mode"  Set Text
    yicesEFGenModes
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "ef-max-iters"           Integer
    1 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      , [Char] -> Integer -> Integer -> [ConfigDesc]
    intWithRangeOpt   [Char]
    "ef-max-samples"         Integer
    0 (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      ]

    -- | This checks that the element is in a logic fragment supported by Yices,
    -- and returns whether the exists-forall solver should be used.
    checkSupportedByYices :: B.BoolExpr t -> IO ProblemFeatures
    checkSupportedByYices :: forall t. BoolExpr t -> IO ProblemFeatures
    checkSupportedByYices BoolExpr t
    p = do
      let varInfo :: CollectedVarInfo t
    varInfo = BoolExpr t -> CollectedVarInfo t
    forall t. Expr t BaseBoolType -> CollectedVarInfo t
    predicateVarInfo BoolExpr t
    p

      -- Check no errors where reported in result.
      let errors :: [Doc Void]
    errors = Seq (Doc Void) -> [Doc Void]
    forall a. Seq a -> [a]
    forall (t :: Type -> Type) a. Foldable t => t a -> [a]
    toList (CollectedVarInfo t
    varInfoCollectedVarInfo t
    -> Getting (Seq (Doc Void)) (CollectedVarInfo t) (Seq (Doc Void))
    -> Seq (Doc Void)
    forall s a. s -> Getting a s a -> a
    ^.Getting (Seq (Doc Void)) (CollectedVarInfo t) (Seq (Doc Void))
    forall t (f :: Type -> Type).
    Functor f =>
    (Seq (Doc Void) -> f (Seq (Doc Void)))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    varErrors)
      Bool -> IO () -> IO ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (Bool -> Bool
    not ([Doc Void] -> Bool
    forall a. [a] -> Bool
    forall (t :: Type -> Type) a. Foldable t => t a -> Bool
    null [Doc Void]
    errors)) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> IO ()
    forall a. [Char] -> IO a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc Void -> [Char]
    forall a. Show a => a -> [Char]
    show (Doc Void -> [Char]) -> Doc Void -> [Char]
    forall a b. (a -> b) -> a -> b
    $
          [Doc Void] -> Doc Void
    forall ann. [Doc ann] -> Doc ann
    PP.vcat [Doc Void
    "This formula is not supported by yices:", Int -> Doc Void -> Doc Void
    forall ann. Int -> Doc ann -> Doc ann
    PP.indent Int
    2 ([Doc Void] -> Doc Void
    forall ann. [Doc ann] -> Doc ann
    PP.vcat [Doc Void]
    errors)]

      ProblemFeatures -> IO ProblemFeatures
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (ProblemFeatures -> IO ProblemFeatures)
    -> ProblemFeatures -> IO ProblemFeatures
    forall a b. (a -> b) -> a -> b
    $! CollectedVarInfo t
    varInfoCollectedVarInfo t
    -> Getting ProblemFeatures (CollectedVarInfo t) ProblemFeatures
    -> ProblemFeatures
    forall s a. s -> Getting a s a -> a
    ^.Getting ProblemFeatures (CollectedVarInfo t) ProblemFeatures
    forall t (f :: Type -> Type).
    Functor f =>
    (ProblemFeatures -> f ProblemFeatures)
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    problemFeatures

    -- | Write a yices file that checks the satisfiability of the given predicate.
    writeYicesFile :: B.ExprBuilder t st fs -- ^ Builder for getting current bindings.
                   -> FilePath              -- ^ Path to file
                   -> B.BoolExpr t          -- ^ Predicate to check
                   -> IO ()
    writeYicesFile :: forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> [Char] -> BoolExpr t -> IO ()
    writeYicesFile ExprBuilder t st fs
    sym [Char]
    path BoolExpr t
    p = do
      [Char] -> IOMode -> (Handle -> IO ()) -> IO ()
    forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
    withFile [Char]
    path IOMode
    WriteMode ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ \Handle
    h -> do
        let cfg :: Config
    cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
        let varInfo :: CollectedVarInfo t
    varInfo = BoolExpr t -> CollectedVarInfo t
    forall t. Expr t BaseBoolType -> CollectedVarInfo t
    predicateVarInfo BoolExpr t
    p
        -- check whether to use ef-solve
        let features :: ProblemFeatures
    features = CollectedVarInfo t
    varInfoCollectedVarInfo t
    -> Getting ProblemFeatures (CollectedVarInfo t) ProblemFeatures
    -> ProblemFeatures
    forall s a. s -> Getting a s a -> a
    ^.Getting ProblemFeatures (CollectedVarInfo t) ProblemFeatures
    forall t (f :: Type -> Type).
    Functor f =>
    (ProblemFeatures -> f ProblemFeatures)
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    problemFeatures
        let efSolver :: Bool
    efSolver = ProblemFeatures
    features ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useExistForall

        bindings <- ExprBuilder t st fs -> IO (SymbolVarBimap t)
    forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> IO (SymbolVarBimap t)
    B.getSymbolVarBimap ExprBuilder t st fs
    sym

        str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
        in_str <- Streams.nullInput
        let t = Integer -> SolverGoalTimeout
    SolverGoalTimeout Integer
    0  -- no timeout needed; not doing actual solving
        c <- newConnection str in_str (const nullAcknowledgementAction) features t bindings
        setYicesParams c cfg
        assume c p
        if efSolver then
          addCommandNoAck c efSolveCommand
        else
          sendCheck c
        sendShowModel c

    -- | Run writer and get a yices result.
    runYicesInOverride :: B.ExprBuilder t st fs
                       -> LogData
                       -> [B.BoolExpr t]
                       -> (SatResult (GroundEvalFn t) () -> IO a)
                       -> IO a
    runYicesInOverride :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t) () -> IO a)
    -> IO a
    runYicesInOverride ExprBuilder t st fs
    sym LogData
    logData [BoolExpr t]
    conditions SatResult (GroundEvalFn t) () -> IO a
    resultFn = do
      let cfg :: Config
    cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
      yices_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
    findSolverPath ConfigOption (BaseStringType Unicode)
    yicesPath Config
    cfg
      condition <- andAllOf sym folded conditions

      logCallbackVerbose logData 2 "Calling Yices to check sat"
      -- Check Problem features
      logSolverEvent sym
        (SolverStartSATQuery $ SolverStartSATQueryRec
        { satQuerySolverName = "Yices"
        , satQueryReason = logReason logData
        })
      features <- checkSupportedByYices condition
      enableMCSat <- getOpt =<< getOptionSetting yicesEnableMCSat cfg
      goalTimeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting yicesGoalTimeout cfg)
      let efSolver = ProblemFeatures
    features ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useExistForall
      let nlSolver = ProblemFeatures
    features ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useNonlinearArithmetic
      let args0 | Bool
    efSolver  = [[Char]
    "--mode=ef"] -- ,"--print-success"]
                | Bool
    nlSolver  = [[Char]
    "--logic=QF_NRA"] -- ,"--print-success"]
                | Bool
    otherwise = [[Char]
    "--mode=one-shot"] -- ,"--print-success"]
      let args = [[Char]]
    args0 [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ if Bool
    enableMCSat then [[Char]
    "--mcsat"] else []
          hasNamedAssumptions = ProblemFeatures
    features ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useUnsatCores Bool -> Bool -> Bool
    ||
                                ProblemFeatures
    features ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useUnsatAssumptions
      when (enableMCSat && hasNamedAssumptions) $
         fail "Unsat cores and named assumptions are incompatible with MC-SAT in Yices."

      withProcessHandles yices_path args Nothing $ \hdls :: (Handle, Handle, Handle, ProcessHandle)
    hdls@(Handle
    in_h, Handle
    out_h, Handle
    err_h, ProcessHandle
    ph) -> do

          (in_stream, out_stream, err_reader) <-
            Handle
    -> Handle
    -> Handle
    -> Maybe (Text, Handle)
    -> IO (OutputStream Text, InputStream Text, HandleReader)
    demuxProcessHandles Handle
    in_h Handle
    out_h Handle
    err_h
              ((Handle -> (Text, Handle)) -> Maybe Handle -> Maybe (Text, Handle)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\Handle
    x -> (Text
    "; ",Handle
    x)) (Maybe Handle -> Maybe (Text, Handle))
    -> Maybe Handle -> Maybe (Text, Handle)
    forall a b. (a -> b) -> a -> b
    $ LogData -> Maybe Handle
    logHandle LogData
    logData)

          -- Create new connection for sending commands to yices.
          bindings <- B.getSymbolVarBimap sym

          c <- newConnection in_stream out_stream (const nullAcknowledgementAction) features goalTimeout bindings
          -- Write yices parameters.
          setYicesParams c cfg
          -- Assert condition
          assume c condition

          logCallbackVerbose logData 2 "Running check sat"
          if efSolver then
            addCommandNoAck c efSolveCommand
          else
            sendCheck c

          let yp = SolverProcess { solverConn :: WriterConn t Connection
    solverConn = WriterConn t Connection
    c
                                 , solverCleanupCallback :: IO ExitCode
    solverCleanupCallback = (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
    cleanupProcess (Handle, Handle, Handle, ProcessHandle)
    hdls
                                 , solverHandle :: ProcessHandle
    solverHandle = ProcessHandle
    ph
                                 , solverErrorBehavior :: ErrorBehavior
    solverErrorBehavior = ErrorBehavior
    ImmediateExit
                                 , solverStderr :: HandleReader
    solverStderr = HandleReader
    err_reader
                                 , solverEvalFuns :: SMTEvalFunctions Connection
    solverEvalFuns = WriterConn t Connection
    -> InputStream Text -> SMTEvalFunctions Connection
    forall h t.
    SMTReadWriter h =>
    WriterConn t h -> InputStream Text -> SMTEvalFunctions h
    forall t.
    WriterConn t Connection
    -> InputStream Text -> SMTEvalFunctions Connection
    smtEvalFuns WriterConn t Connection
    c InputStream Text
    out_stream
                                 , solverName :: [Char]
    solverName = [Char]
    "Yices"
                                 , solverLogFn :: SolverEvent -> IO ()
    solverLogFn = ExprBuilder t st fs -> SolverEvent -> IO ()
    forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
    logSolverEvent ExprBuilder t st fs
    sym
                                 , solverEarlyUnsat :: IORef (Maybe Int)
    solverEarlyUnsat = Connection -> IORef (Maybe Int)
    yicesEarlyUnsat (WriterConn t Connection -> Connection
    forall t h. WriterConn t h -> h
    connState WriterConn t Connection
    c)
                                 , solverSupportsResetAssertions :: Bool
    solverSupportsResetAssertions = Bool
    True
                                 , solverGoalTimeout :: SolverGoalTimeout
    solverGoalTimeout = SolverGoalTimeout
    goalTimeout
                                 }
          sat_result <- getSatResult yp
          logSolverEvent sym
            (SolverEndSATQuery $ SolverEndSATQueryRec
            { satQueryResult = sat_result
            , satQueryError  = Nothing
            })
          r <-
             case sat_result of
               Sat () -> SatResult (GroundEvalFn t) () -> IO a
    resultFn (SatResult (GroundEvalFn t) () -> IO a)
    -> (GroundEvalFn t -> SatResult (GroundEvalFn t) ())
    -> GroundEvalFn t
    -> IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . GroundEvalFn t -> SatResult (GroundEvalFn t) ()
    forall mdl core. mdl -> SatResult mdl core
    Sat (GroundEvalFn t -> IO a) -> IO (GroundEvalFn t) -> IO a
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SolverProcess t Connection -> IO (GroundEvalFn t)
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO (GroundEvalFn scope)
    getModel SolverProcess t Connection
    yp
               Unsat ()
    x -> SatResult (GroundEvalFn t) () -> IO a
    resultFn (() -> SatResult (GroundEvalFn t) ()
    forall mdl core. core -> SatResult mdl core
    Unsat ()
    x)
               SatResult () ()
    Unknown -> SatResult (GroundEvalFn t) () -> IO a
    resultFn SatResult (GroundEvalFn t) ()
    forall mdl core. SatResult mdl core
    Unknown

          _ <- yicesShutdownSolver yp
          return r