------------------------------------------------------------------------
-- |
-- 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 ->
      forall (m :: Type -> Type) a. Monad m => a -> m a
return (if Bool
x then Builder
"true" else Builder
"false")
  ConcreteReal Rational
x ->
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
decimal (forall a. Ratio a -> a
numerator Rational
x) forall a. Semigroup a => a -> a -> a
<> Builder
"/" forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
decimal (forall a. Ratio a -> a
denominator Rational
x)
  ConcreteInteger Integer
x ->
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
decimal Integer
x
  ConcreteString (UnicodeLiteral Text
x) ->
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Text -> Builder
Builder.fromText Text
x
  ConcreteVal tp
_ ->
      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 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    = forall v. SupportTermOps v => v -> v -> v -> v
ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
">=" YicesTerm
x YicesTerm
0) YicesTerm
x (forall a. Num a => a -> a
negate YicesTerm
x)
  signum :: YicesTerm -> YicesTerm
signum YicesTerm
x = forall v. SupportTermOps v => v -> v -> v -> v
ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"=" YicesTerm
x YicesTerm
0) YicesTerm
0 forall a b. (a -> b) -> a -> b
$ forall v. SupportTermOps v => v -> v -> v -> v
ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
">" YicesTerm
x YicesTerm
0) YicesTerm
1 (forall a. Num a => a -> a
negate YicesTerm
1)
  fromInteger :: Integer -> YicesTerm
fromInteger Integer
i = Builder -> YicesTerm
T (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 (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 = forall a. Integral a => a -> YicesTerm
decimal_term (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 forall a. Semigroup a => a -> a -> a
<> Builder
"::" forall a. Semigroup a => a -> a -> a
<> YicesType -> Builder
unType (forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome 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 forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"lambda" [ [Builder] -> Builder
builder_list (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Some TypeMap -> Builder
varBinding 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 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" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> YicesTerm -> Builder
letBinding 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 = forall a. a -> a
id
  termRealToInteger :: YicesTerm -> YicesTerm
termRealToInteger = forall a. a -> a
id

  integerTerm :: Integer -> YicesTerm
integerTerm Integer
i = Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ 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 forall v. SupportTermOps v => v -> v -> v
.== forall v. SupportTermOps v => Integer -> v
integerTerm Integer
0
  intDivisible YicesTerm
x Nat
k = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"divides" [forall v. SupportTermOps v => Integer -> v
integerTerm (forall a. Integral a => a -> Integer
toInteger Nat
k), YicesTerm
x]

  rationalTerm :: Rational -> YicesTerm
rationalTerm Rational
r | Integer
d forall a. Eq a => a -> a -> Bool
== Integer
1    = Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
decimal Integer
n
                 | Bool
otherwise = Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"/" [forall a. Integral a => a -> Builder
decimal Integer
n, forall a. Integral a => a -> Builder
decimal Integer
d]
    where n :: Integer
n = forall a. Ratio a -> a
numerator Rational
r
          d :: Integer
d = 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" [forall (n :: Nat). NatRepr n -> YicesTerm
width_term NatRepr w
w, forall a. Integral a => a -> YicesTerm
decimal_term Integer
d]
    where d :: Integer
d = 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 = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Nat
n forall a. Ord a => a -> a -> Bool
> Nat
0) forall a b. (a -> b) -> a -> b
$
    let -- Get index of bit to end at (least-significant bit has index 0)
        end :: YicesTerm
end = forall a. Integral a => a -> YicesTerm
decimal_term (Nat
bforall a. Num a => a -> a -> a
+Nat
nforall a. Num a => a -> a -> a
-Nat
1)
        -- Get index of bit to start at (least-significant bit has index 0)
        begin :: YicesTerm
begin = 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 = forall a. a
errorComputableUnsupported
  realCos :: YicesTerm -> YicesTerm
realCos = forall a. a
errorComputableUnsupported
  realTan :: YicesTerm -> YicesTerm
realTan = forall a. a
errorComputableUnsupported
  realATan2 :: YicesTerm -> YicesTerm -> YicesTerm
realATan2 = forall a. a
errorComputableUnsupported
  realSinh :: YicesTerm -> YicesTerm
realSinh = forall a. a
errorComputableUnsupported
  realCosh :: YicesTerm -> YicesTerm
realCosh = forall a. a
errorComputableUnsupported
  realTanh :: YicesTerm -> YicesTerm
realTanh = forall a. a
errorComputableUnsupported
  realExp :: YicesTerm -> YicesTerm
realExp = forall a. a
errorComputableUnsupported
  realLog :: YicesTerm -> YicesTerm
realLog = 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 = forall a. Maybe a
Nothing

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

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

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

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

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

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

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

  floatCast :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
floatCast       FloatPrecisionRepr fpp
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
  floatRound :: RoundingMode -> YicesTerm -> YicesTerm
floatRound      RoundingMode
_ YicesTerm
_   = forall a. (?callStack::CallStack) => a
floatFail
  floatFromBinary :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> YicesTerm -> YicesTerm
floatFromBinary FloatPrecisionRepr fpp
_ YicesTerm
_   = forall a. (?callStack::CallStack) => a
floatFail
  bvToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
bvToFloat       FloatPrecisionRepr fpp
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
  sbvToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
sbvToFloat      FloatPrecisionRepr fpp
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
  realToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
realToFloat     FloatPrecisionRepr fpp
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
  floatToBV :: Nat -> RoundingMode -> YicesTerm -> YicesTerm
floatToBV       Nat
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
  floatToSBV :: Nat -> RoundingMode -> YicesTerm -> YicesTerm
floatToSBV      Nat
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
  floatToReal :: YicesTerm -> YicesTerm
floatToReal     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 = forall a. (?callStack::CallStack) => [Char] -> a
error ([Char]
"Yices does not support " forall a. Semigroup a => a -> a -> a
<> [Char]
s)

floatFail :: HasCallStack => a
floatFail :: forall a. (?callStack::CallStack) => a
floatFail = 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 = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"Yices does not support strings"

errorComputableUnsupported :: a
errorComputableUnsupported :: forall a. a
errorComputableUnsupported = 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 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 forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"->" (YicesType -> Builder
unType forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ([YicesType]
args 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" [forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show NatRepr w
w)])
yicesType (FloatTypeMap FloatPrecisionRepr fpp
_) = forall a. (?callStack::CallStack) => a
floatFail
yicesType TypeMap tp
UnicodeTypeMap = 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 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]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap (idxl ::> idx)
i) (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 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]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap (idxl ::> idx)
i) (forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType TypeMap tp1
r)
yicesType (StructTypeMap Assignment TypeMap idx
f)      = [YicesType] -> YicesType
tupleType (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]
toListFC 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 = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd 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" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> YicesType -> Builder
mkBinding 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 forall a. Semigroup a => a -> a -> a
<> 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 forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"eval" [YicesTerm -> Builder
renderTerm Term Connection
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 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 forall a b. (a -> b) -> a -> b
$
   Builder -> [Builder] -> Builder
app Builder
"set-timeout" [ [Char] -> Builder
Builder.fromString (forall a. Show a => a -> [Char]
show (SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds forall a b. (a -> b) -> a -> b
$ Connection -> SolverGoalTimeout
yicesTimeout Connection
conn)) ]

declareUnitTypeCommand :: Command Connection
declareUnitTypeCommand :: Command Connection
declareUnitTypeCommand Connection
_conn = Builder -> YicesCommand
safeCmd 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 Bool
done <- forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef (Connection -> IORef Bool
yicesUnitDeclared (forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn)) (\Bool
x -> (Bool
True, Bool
x))
     forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless Bool
done forall a b. (a -> b) -> a -> b
$ forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t Connection
conn Command Connection
declareUnitTypeCommand

resetUnitType :: WriterConn t Connection -> IO ()
resetUnitType :: forall t. WriterConn t Connection -> IO ()
resetUnitType WriterConn t Connection
conn =
  forall a. IORef a -> a -> IO ()
writeIORef (Connection -> IORef Bool
yicesUnitDeclared (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 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
                  forall a. Bits a => a -> a -> a
.|. Bool -> ProblemFeatures -> ProblemFeatures
featureIf Bool
efSolver ProblemFeatures
useExistForall
                  forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStructs
                  forall a. Bits a => a -> a -> a
.|. (ProblemFeatures
reqFeatures forall a. Bits a => a -> a -> a
.&. (ProblemFeatures
useUnsatCores forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useUnsatAssumptions))

  IORef (Maybe Int)
earlyUnsatRef <- forall a. a -> IO (IORef a)
newIORef forall a. Maybe a
Nothing
  IORef Bool
unitRef <- forall a. a -> IO (IORef a)
newIORef Bool
False
  let c :: Connection
c = Connection { yicesEarlyUnsat :: IORef (Maybe Int)
yicesEarlyUnsat = IORef (Maybe Int)
earlyUnsatRef
                     , yicesTimeout :: SolverGoalTimeout
yicesTimeout = SolverGoalTimeout
timeout
                     , yicesUnitDeclared :: IORef Bool
yicesUnitDeclared = IORef Bool
unitRef
                     }
  WriterConn t Connection
conn <- forall t cs.
OutputStream Text
-> InputStream Text
-> AcknowledgementAction t cs
-> [Char]
-> ResponseStrictness
-> ProblemFeatures
-> SymbolVarBimap t
-> cs
-> IO (WriterConn t cs)
newWriterConn OutputStream Text
stream InputStream Text
in_stream (IORef (Maybe Int) -> AcknowledgementAction t Connection
ack IORef (Maybe Int)
earlyUnsatRef) [Char]
nm ResponseStrictness
Strict ProblemFeatures
features' SymbolVarBimap t
bindings Connection
c
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! WriterConn t Connection
conn { supportFunctionDefs :: Bool
supportFunctionDefs = Bool
True
                 , supportFunctionArguments :: Bool
supportFunctionArguments = Bool
True
                 , supportQuantifiers :: Bool
supportQuantifiers = Bool
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" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Some TypeMap -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
vars) Term Connection
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" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Some TypeMap -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
vars) Term Connection
t

  arraySelect :: Term Connection -> [Term Connection] -> Term Connection
arraySelect = 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 forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"update" [ YicesTerm -> Builder
renderTerm Term Connection
a, [Builder] -> Builder
builder_list (YicesTerm -> Builder
renderTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term Connection]
i), YicesTerm -> Builder
renderTerm Term Connection
v ]

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

  pushCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
pushCommand f Connection
_   = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(push)"
  popCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
popCommand f Connection
_    = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(pop)"
  push2Command :: forall (f :: Type -> Type). f Connection -> Command Connection
push2Command f Connection
_   = forall a. [Char] -> a
unsupportedFeature [Char]
"(push 2)"
  pop2Command :: forall (f :: Type -> Type). f Connection -> Command Connection
pop2Command f Connection
_    = forall a. [Char] -> a
unsupportedFeature [Char]
"(pop 2)"
  resetCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
resetCommand f Connection
_  = forall a b. a -> b -> a
const 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, forall a b. a -> b -> a
const 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
    , forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app_list Builder
"check-assuming" (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
_ = forall a b. a -> b -> a
const 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
_ = forall a b. a -> b -> a
const 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
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"abduction"
  getAbductNextCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
getAbductNextCommand f Connection
_ = 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) = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd 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 = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd 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 =
    forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$
    Builder -> [Builder] -> Builder
app Builder
"define" [Text -> Builder
Builder.fromText Text
v forall a. Semigroup a => a -> a -> a
<> Builder
"::"
                  forall a. Semigroup a => a -> a -> a
<> YicesType -> Builder
unType ([YicesType] -> YicesType -> YicesType
fnType (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]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap args
args) (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 =
    forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$
    Builder -> [Builder] -> Builder
app Builder
"define" [Text -> Builder
Builder.fromText Text
v forall a. Semigroup a => a -> a -> a
<> Builder
"::"
                  forall a. Semigroup a => a -> a -> a
<> YicesType -> Builder
unType ([YicesType] -> YicesType -> YicesType
fnType ((\(Text
_,Some TypeMap
tp) -> forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Some TypeMap
tp) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
args) (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
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
_ = 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
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"SyGuS"
  constraintCommand :: forall (f :: Type -> Type).
f Connection -> Term Connection -> Command Connection
constraintCommand f Connection
_ Term Connection
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"SyGuS"

  resetDeclaredStructs :: forall t. WriterConn t Connection -> IO ()
resetDeclaredStructs WriterConn t Connection
conn = 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
s, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index args tp
i 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]
args

  stringTerm :: Text -> Term Connection
stringTerm Text
_   = forall a. (?callStack::CallStack) => a
stringFail
  stringLength :: Term Connection -> Term Connection
stringLength Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
  stringAppend :: [Term Connection] -> Term Connection
stringAppend [Term Connection]
_ = forall a. (?callStack::CallStack) => a
stringFail
  stringContains :: Term Connection -> Term Connection -> Term Connection
stringContains Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
  stringIndexOf :: Term Connection
-> Term Connection -> Term Connection -> Term Connection
stringIndexOf Term Connection
_ Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
  stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection
stringIsPrefixOf Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
  stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection
stringIsSuffixOf Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
  stringSubstring :: Term Connection
-> Term Connection -> Term Connection -> Term Connection
stringSubstring Term Connection
_ Term Connection
_ Term Connection
_ = 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 = forall t. WriterConn t Connection -> IO ()
declareUnitType WriterConn t Connection
conn
  declareStructDatatype WriterConn t Connection
_ Assignment TypeMap args
_ = 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 Maybe Int
isEarlyUnsat <- forall a. IORef a -> IO a
readIORef (Connection -> IORef (Maybe Int)
yicesEarlyUnsat (forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn))
       forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (forall a. Maybe a -> Bool
isJust Maybe Int
isEarlyUnsat Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
earlyUnsatSafe) forall a b. (a -> b) -> a -> b
$ do
         forall a. Maybe a -> OutputStream a -> IO ()
Streams.write (forall a. a -> Maybe a
Just Text
cmdout) (forall t h. WriterConn t h -> OutputStream Text
connHandle WriterConn t Connection
conn)
         -- force a flush
         forall a. Maybe a -> OutputStream a -> IO ()
Streams.write (forall a. a -> Maybe a
Just Text
"") (forall t h. WriterConn t h -> OutputStream Text
connHandle WriterConn t Connection
conn)
    where
      cmd :: YicesCommand
cmd = Command Connection
cmdf (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 = Text -> Text
Lazy.toStrict (Builder -> Text
Builder.toLazyText Builder
cmdBuilder) 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    = 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 -> 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    = 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
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Yices does not support floats."
                     , smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper Connection)
smtEvalBvArray = forall a. Maybe a
Nothing
                     , smtEvalString :: Term Connection -> IO Text
smtEvalString  = \Term Connection
_ -> 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
_ = 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 Either SomeException SExp
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t Connection
s))
       let cmd :: YicesCommand
cmd = Builder -> YicesCommand
safeCmd Builder
"(show-unsat-assumptions)"
       case Either SomeException SExp
mb of
         Right (SExp -> Maybe [(Bool, Text)]
asNegAtomList -> Just [(Bool, Text)]
as) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return [(Bool, Text)]
as
         Right (SApp [SAtom Text
"error", SString Text
msg]) -> forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesError YicesCommand
cmd Text
msg)
         Right SExp
res -> forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd ([Char] -> Text
Text.pack (forall a. Show a => a -> [Char]
show SExp
res)))
         Left (SomeException e
e) -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd forall a b. (a -> b) -> a -> b
$ [Char] -> Text
Text.pack forall a b. (a -> b) -> a -> b
$
                 [[Char]] -> [Char]
unlines [ [Char]
"Could not parse unsat assumptions result."
                         , [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ 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 Either SomeException SExp
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t Connection
s))
       let cmd :: YicesCommand
cmd = Builder -> YicesCommand
safeCmd Builder
"(show-unsat-core)"
       case Either SomeException SExp
mb of
         Right (SExp -> Maybe [Text]
asAtomList -> Just [Text]
nms) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return [Text]
nms

         Right (SApp [SAtom Text
"error", SString Text
msg]) -> forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesError YicesCommand
cmd Text
msg)
         Right SExp
res -> forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd ([Char] -> Text
Text.pack (forall a. Show a => a -> [Char]
show SExp
res)))
         Left (SomeException e
e) -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd forall a b. (a -> b) -> a -> b
$ [Char] -> Text
Text.pack forall a b. (a -> b) -> a -> b
$
                 [[Char]] -> [Char]
unlines [ [Char]
"Could not parse unsat core result."
                         , [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ 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
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"abduction"

  smtAbductNextResult :: forall (f :: Type -> Type) t.
f Connection -> WriterConn t Connection -> IO [Char]
smtAbductNextResult f Connection
_ = 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]
"  " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)
       ]
  show (YicesError (YicesCommand Bool
_ Builder
cmd) Text
msg) =
     [[Char]] -> [Char]
unlines
       [ [Char]
"Solver reported an error:"
       , [Char]
"  " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack Text
msg
       , [Char]
"in response to command:"
       , [Char]
"  " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)
       ]
  show (YicesParseError (YicesCommand Bool
_ Builder
cmd) Text
msg) =
     [[Char]] -> [Char]
unlines
       [ [Char]
"Could not parse solver response:"
       , [Char]
"  " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack Text
msg
       , [Char]
"in response to command:"
       , [Char]
"  " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
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 = 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, Text)
shutdownSolverProcess = forall scope. SolverProcess scope Connection -> IO (ExitCode, Text)
yicesShutdownSolver

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

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

      ExitCode
ec <- forall scope solver. SolverProcess scope solver -> IO ExitCode
solverCleanupCallback SolverProcess s Connection
p
      forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExitCode
ec,Text
txt)


yicesAck ::
  IORef (Maybe Int) ->
  AcknowledgementAction s Connection
yicesAck :: forall s. IORef (Maybe Int) -> AcknowledgementAction s Connection
yicesAck IORef (Maybe Int)
earlyUnsatRef = forall t h.
(WriterConn t h -> Command h -> IO ()) -> AcknowledgementAction t h
AckAction forall a b. (a -> b) -> a -> b
$ \WriterConn s Connection
conn Command Connection
cmdf ->
  do Maybe Int
isEarlyUnsat <- forall a. IORef a -> IO a
readIORef IORef (Maybe Int)
earlyUnsatRef
     let cmd :: YicesCommand
cmd = Command Connection
cmdf (forall t h. WriterConn t h -> h
connState WriterConn s Connection
conn)
         earlyUnsatSafe :: Bool
earlyUnsatSafe = YicesCommand -> Bool
cmdEarlyUnsatSafe YicesCommand
cmd
         cmdBuilder :: Builder
cmdBuilder = YicesCommand -> Builder
cmdCmd YicesCommand
cmd
     if forall a. Maybe a -> Bool
isJust Maybe Int
isEarlyUnsat Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
earlyUnsatSafe
     then forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
     else do
       Maybe Text
x <- InputStream Text -> IO (Maybe Text)
getAckResponse (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn s Connection
conn)
       case Maybe Text
x of
         Maybe Text
Nothing ->
           forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
         Just Text
"unsat" ->
           do Int
i <- forall t h. WriterConn t h -> IO Int
entryStackHeight WriterConn s Connection
conn
              forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe Int)
earlyUnsatRef forall a b. (a -> b) -> a -> b
$! (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! if Int
i forall a. Ord a => a -> a -> Bool
> Int
0 then Int
1 else Int
0)
         Just Text
txt ->
           forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
                   [ [Char]
"Unexpected response from solver while awaiting acknowledgement"
                   , [Char]
"*** result:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Text
txt
                   , [Char]
"in response to command"
                   , [Char]
"***: " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
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 = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
  [Char]
yices_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
findSolverPath ConfigOption (BaseStringType Unicode)
yicesPath Config
cfg
  Bool
enableMCSat <- forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableMCSat Config
cfg
  Bool
enableInteractive <- forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableInteractive Config
cfg
  SolverGoalTimeout
goalTimeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
1000forall a. Num a => a -> a -> a
*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
yicesGoalTimeout Config
cfg)
  let modeFlag :: [Char]
modeFlag | Bool
enableInteractive
                 Bool -> Bool -> Bool
|| (SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds SolverGoalTimeout
goalTimeout) forall a. Eq a => a -> a -> Bool
/= Integer
0 = [Char]
"--mode=interactive"
               | Bool
otherwise = [Char]
"--mode=push-pop"
      args :: [[Char]]
args = [Char]
modeFlag forall a. a -> [a] -> [a]
: [Char]
"--print-success" forall a. a -> [a] -> [a]
:
             if Bool
enableMCSat then [[Char]
"--mcsat"] else []
      hasNamedAssumptions :: Bool
hasNamedAssumptions = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores Bool -> Bool -> Bool
||
                            ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatAssumptions
  forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
enableMCSat Bool -> Bool -> Bool
&& Bool
hasNamedAssumptions) forall a b. (a -> b) -> a -> b
$
     forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Unsat cores and named assumptions are incompatible with MC-SAT in Yices."
  let  features' :: ProblemFeatures
features' | Bool
enableMCSat = ProblemFeatures
features forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useNonlinearArithmetic
                 | Bool
otherwise = ProblemFeatures
features

  hdls :: (Handle, Handle, Handle, ProcessHandle)
hdls@(Handle
in_h,Handle
out_h,Handle
err_h,ProcessHandle
ph) <- [Char]
-> [[Char]]
-> Maybe [Char]
-> IO (Handle, Handle, Handle, ProcessHandle)
startProcess [Char]
yices_path [[Char]]
args forall a. Maybe a
Nothing

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

  OutputStream Text
in_stream' <- forall b a. IO b -> OutputStream a -> IO (OutputStream a)
Streams.atEndOfOutput (Handle -> IO ()
hClose Handle
in_h) OutputStream Text
in_stream

  WriterConn t Connection
conn <- forall t.
OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
newConnection OutputStream Text
in_stream' InputStream Text
out_stream forall s. IORef (Maybe Int) -> AcknowledgementAction s Connection
yicesAck ProblemFeatures
features' SolverGoalTimeout
goalTimeout forall t. SymbolVarBimap t
B.emptySymbolVarBimap

  forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
conn Config
cfg

  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! SolverProcess { solverConn :: WriterConn t Connection
solverConn   = WriterConn t Connection
conn
                          , solverCleanupCallback :: IO ExitCode
solverCleanupCallback = (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
cleanupProcess (Handle, Handle, Handle, ProcessHandle)
hdls
                          , solverStderr :: HandleReader
solverStderr = HandleReader
err_reader
                          , solverHandle :: ProcessHandle
solverHandle = ProcessHandle
ph
                          , solverErrorBehavior :: ErrorBehavior
solverErrorBehavior = ErrorBehavior
ContinueOnError
                          , solverEvalFuns :: SMTEvalFunctions Connection
solverEvalFuns = forall h t.
SMTReadWriter h =>
WriterConn t h -> InputStream Text -> SMTEvalFunctions h
smtEvalFuns WriterConn t Connection
conn InputStream Text
out_stream
                          , solverLogFn :: SolverEvent -> IO ()
solverLogFn = forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
                          , solverName :: [Char]
solverName = [Char]
"Yices"
                          , solverEarlyUnsat :: IORef (Maybe Int)
solverEarlyUnsat = Connection -> IORef (Maybe Int)
yicesEarlyUnsat (forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn)
                          , solverSupportsResetAssertions :: Bool
solverSupportsResetAssertions = Bool
True
                          , solverGoalTimeout :: SolverGoalTimeout
solverGoalTimeout = 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 = forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn t Connection
c (forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands WriterConn t Connection
c)

sendCheckExistsForall :: WriterConn t Connection -> IO ()
sendCheckExistsForall :: forall t. WriterConn t Connection -> IO ()
sendCheckExistsForall WriterConn t Connection
c = 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 = 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 forall (tp :: BaseType). ConfigOption tp -> [Text]
configOptionNameParts ConfigOption tp
o of
    [Text
yicesName, Text
nm] | Text
yicesName forall a. Eq a => a -> a -> Bool
== Text
"yices" ->
      case forall (tp :: BaseType). ConcreteVal tp -> Maybe Builder
asYicesConfigValue ConcreteVal tp
val of
        Just Builder
v ->
          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 ->
          forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"Unknown Yices parameter type:", forall a. Show a => a -> [Char]
show Text
nm]
    [Text]
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"not a Yices parameter", 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
   [ConfigValue]
params <- Text -> Config -> IO [ConfigValue]
getConfigValues Text
"yices" Config
cfg
   forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ConfigValue]
params forall a b. (a -> b) -> a -> b
$ forall t. WriterConn t Connection -> ConfigValue -> IO ()
setParam WriterConn t Connection
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 = 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 = 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 Either SomeException SExp
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) InputStream Text
resps)
     case Either SomeException SExp
mb of
       Right (SAtom Text
"ok") -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
       Right (SAtom Text
txt)  -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Text
txt)
       Right SExp
res -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$
               [[Char]] -> [Char]
unlines [ [Char]
"Could not parse acknowledgement result."
                       , [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SExp
res
                       ]
       Left (SomeException e
e) -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$
               [[Char]] -> [Char]
unlines [ [Char]
"Could not parse acknowledgement result."
                       , [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ 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")   -> forall mdl core. core -> SatResult mdl core
Unsat ()
        (SAtom Text
"sat")     -> forall mdl core. mdl -> SatResult mdl core
Sat ()
        (SAtom Text
"unknown") -> forall mdl core. SatResult mdl core
Unknown
        (SAtom Text
"interrupted") -> forall mdl core. SatResult mdl core
Unknown
        SExp
res -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ [Char] -> UnparseableYicesResponse
UnparseableYicesResponse forall a b. (a -> b) -> a -> b
$
               [[Char]] -> [Char]
unlines [ [Char]
"Could not parse sat result."
                       , [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SExp
res
                       ]
      tmo :: Integer
tmo = SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds forall a b. (a -> b) -> a -> b
$ Connection -> SolverGoalTimeout
yicesTimeout forall a b. (a -> b) -> a -> b
$ 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 forall a. Num a => a -> a -> a
*)
      deadman_tmo :: Int
deadman_tmo = Int -> Int
msec2usec forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger (Integer
tmo forall a. Num a => a -> a -> a
+ Integer
delay)
      deadmanTimer :: IO ()
deadmanTimer = Int -> IO ()
threadDelay Int
deadman_tmo
      action :: InputStream Text -> IO SExp
action = forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString)
  in if Integer
tmo forall a. Eq a => a -> a -> Bool
== Integer
0
     then 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 (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t Connection
conn)) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Right SExp
d -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SExp -> SatResult () ()
interpretSExpr SExp
d
            Left SomeException
e -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Could not parse sat result."
                                     , [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException SomeException
e
                                     ]
     else forall a b. IO a -> IO b -> IO (Either a b)
race IO ()
deadmanTimer (forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync forall a b. (a -> b) -> a -> b
$ InputStream Text -> IO SExp
action (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t Connection
conn)) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Right (Right SExp
x) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SExp -> SatResult () ()
interpretSExpr SExp
x
          Left () -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall mdl core. SatResult mdl core
Unknown  -- no response in timeout period
          Right (Left SomeException
e) -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Could not parse sat result."
                                           , [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException SomeException
e
                                           ]

data UnparseableYicesResponse = UnparseableYicesResponse String deriving Int -> UnparseableYicesResponse -> ShowS
[UnparseableYicesResponse] -> ShowS
UnparseableYicesResponse -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [UnparseableYicesResponse] -> ShowS
$cshowList :: [UnparseableYicesResponse] -> ShowS
show :: UnparseableYicesResponse -> [Char]
$cshow :: UnparseableYicesResponse -> [Char]
showsPrec :: Int -> UnparseableYicesResponse -> ShowS
$cshowsPrec :: Int -> UnparseableYicesResponse -> ShowS
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 forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn s Connection
conn Term Connection
tm
     Either SomeException (Root Rational)
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser ()
skipSpaceOrNewline forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Text (Root Rational)
Root.parseYicesRoot) InputStream Text
resp)
     case Either SomeException (Root Rational)
mb of
       Left (SomeException e
ex) ->
           forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
             [ [Char]
"Could not parse real value returned by yices: "
             , forall e. Exception e => e -> [Char]
displayException e
ex
             ]
       Right Root Rational
r -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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
'\"' 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 [Char]
ds <- forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
Atto.choice [ 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 forall a. (Eq a, Num a) => ReadS a
readOct [Char]
ds of
        (Int
c,[Char]
""):[(Int, [Char])]
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Char -> Text
Text.singleton (forall a. Enum a => Int -> a
toEnum Int
c))
        [(Int, [Char])]
_ -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero

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

 go :: Parser Text
go = do Text
xs <- (Char -> Bool) -> Parser Text
Atto.takeWhile Char -> Bool
isStringChar
         (Char -> Parser Char
Atto.char Char
'\"' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return Text
xs)
          forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (do Char
_ <- Char -> Parser Char
Atto.char Char
'\\'
                  Text
e <- Parser Text
escape
                  Text
ys <- Parser Text
go
                  forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
xs forall a. Semigroup a => a -> a -> a
<> Text
e forall a. Semigroup a => a -> a -> a
<> Text
ys))

boolValue :: Atto.Parser Bool
boolValue :: Parser Bool
boolValue =
  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" forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
  , Text -> Parser Text
Atto.string Text
"false" forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> 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 forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn s Connection
conn Term Connection
tm
     Either SomeException Bool
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser ()
skipSpaceOrNewline forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Bool
boolValue) InputStream Text
resp)
     case Either SomeException Bool
mb of
       Left (SomeException e
ex) ->
           forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
             [ [Char]
"Could not parse boolean value returned by yices: "
             , forall e. Exception e => e -> [Char]
displayException e
ex
             ]
       Right Bool
b -> 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
_ <- Text -> Parser Text
Atto.string Text
"0b"
     Text
digits <- (Char -> Bool) -> Parser Text
Atto.takeWhile (forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` ([Char]
"01"::String))
     forall (m :: Type -> Type).
MonadFail m =>
Int -> [Char] -> m Integer
readBit Int
w (Text -> [Char]
Text.unpack Text
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 forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn s Connection
conn Term Connection
tm
     Either SomeException Integer
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser ()
skipSpaceOrNewline forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Int -> Parser Integer
yicesBV (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w)) InputStream Text
resp)
     case Either SomeException Integer
mb of
       Left (SomeException e
ex) ->
           forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
             [ [Char]
"Could not parse bitvector value returned by yices: "
             , forall e. Exception e => e -> [Char]
displayException e
ex
             ]
       Right Integer
b -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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
          forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Eq a => a -> a -> Bool
/= Int
w0) forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Value has a different number of bits than we expected."
          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
nforall a. Num a => a -> a -> a
+Int
1) (Integer
v forall a. Bits a => a -> Int -> a
`shiftL` Int
1)       [Char]
r
            Char
'1' -> Int -> Integer -> [Char] -> m Integer
go (Int
nforall a. Num a => a -> a -> a
+Int
1) ((Integer
v forall a. Bits a => a -> Int -> a
`shiftL` Int
1) forall a. Num a => a -> a -> a
+ Integer
1) [Char]
r
            Char
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Not a bitvector."

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

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

yicesDefaultFeatures :: ProblemFeatures
yicesDefaultFeatures :: ProblemFeatures
yicesDefaultFeatures
    = ProblemFeatures
useIntegerArithmetic
  forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
  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 ->
       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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (GroundEvalFn t
x,forall a. Maybe a
Nothing)) 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 =
       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 (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
yicesStrictParsing)
   }

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

yicesBranchingChoices :: Set Text
yicesBranchingChoices :: Set Text
yicesBranchingChoices = 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 = 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' (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
BaseBoolRepr ([Char]
"solver.yices."forall a. [a] -> [a] -> [a]
++[Char]
nm))
  in [ ConfigDesc
b
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
b] forall a b. (a -> b) -> a -> b
$ ConfigOption BaseBoolType -> ConfigDesc
booleanOpt' (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
BaseBoolRepr ([Char]
"yices."forall a. [a] -> [a] -> [a]
++[Char]
nm))
     ]

booleanOpt' :: ConfigOption BaseBoolType -> ConfigDesc
booleanOpt' :: ConfigOption BaseBoolType -> ConfigDesc
booleanOpt' ConfigOption BaseBoolType
o =
  forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseBoolType
o
        OptionStyle BaseBoolType
boolOptSty
        forall a. Maybe a
Nothing
        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 = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr 'BaseRealType
BaseRealRepr forall a b. (a -> b) -> a -> b
$ [Char]
nforall a. [a] -> [a] -> [a]
++[Char]
nm)
              (Bound Rational -> Bound Rational -> OptionStyle 'BaseRealType
realWithRangeOptSty (forall r. r -> Bound r
Inclusive Rational
lo) (forall r. r -> Bound r
Inclusive Rational
hi))
              forall a. Maybe a
Nothing
              forall a. Maybe a
Nothing
      f :: ConfigDesc
f = [Char] -> ConfigDesc
mkO [Char]
"solver.yices."
  in [ ConfigDesc
f
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
f] 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 = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr 'BaseRealType
BaseRealRepr forall a b. (a -> b) -> a -> b
$ [Char]
nforall a. [a] -> [a] -> [a]
++[Char]
nm)
              (Bound Rational -> OptionStyle 'BaseRealType
realWithMinOptSty Bound Rational
lo)
              forall a. Maybe a
Nothing
              forall a. Maybe a
Nothing
      f :: ConfigDesc
f = [Char] -> ConfigDesc
mkO [Char]
"solver.yices."
  in [ ConfigDesc
f
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
f] 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 = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
BaseIntegerRepr forall a b. (a -> b) -> a -> b
$ [Char]
nforall a. [a] -> [a] -> [a]
++[Char]
nm)
              (Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
integerWithRangeOptSty (forall r. r -> Bound r
Inclusive Integer
lo) (forall r. r -> Bound r
Inclusive Integer
hi))
              forall a. Maybe a
Nothing
              forall a. Maybe a
Nothing
      i :: ConfigDesc
i = [Char] -> ConfigDesc
mkO [Char]
"solver.yices."
  in [ ConfigDesc
i
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
i] 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 = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption (forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr Unicode
UnicodeRepr) forall a b. (a -> b) -> a -> b
$ [Char]
nforall a. [a] -> [a] -> [a]
++[Char]
nm)
              (Set Text -> OptionStyle (BaseStringType Unicode)
enumOptSty Set Text
xs)
              forall a. Maybe a
Nothing
              forall a. Maybe a
Nothing
      e :: ConfigDesc
e = [Char] -> ConfigDesc
mkO [Char]
"solver.yices."
  in [ ConfigDesc
e
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
e] forall a b. (a -> b) -> a -> b
$ [Char] -> ConfigDesc
mkO [Char]
"yices."
     ]

yicesInternalOptions :: [ConfigDesc]
yicesInternalOptions :: [ConfigDesc]
yicesInternalOptions = 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
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Bound Rational -> [ConfigDesc]
floatWithMinOpt   [Char]
"c-factor"    (forall r. r -> Bound r
Inclusive Rational
1)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"d-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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"    (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" (forall a. Num a => a -> a
negate (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)) (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"max-bool-ack"           Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"aux-eq-quota"           Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Bound Rational -> [ConfigDesc]
floatWithMinOpt   [Char]
"aux-eq-ratio"           (forall r. r -> Bound r
Exclusive Rational
0)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"dyn-ack-threshold"      Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
16::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"dyn-bool-ack-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
16::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"max-interface-eqs"      Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"max-update-conflicts"   Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"max-extensionality"     Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
  , [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt   [Char]
"ef-max-samples"         Integer
0 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)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 = forall t. Expr t BaseBoolType -> CollectedVarInfo t
predicateVarInfo BoolExpr t
p

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

  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! CollectedVarInfo t
varInfoforall s a. s -> Getting a s a -> a
^.forall t. Simple Lens (CollectedVarInfo t) ProblemFeatures
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
  forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
withFile [Char]
path IOMode
WriteMode forall a b. (a -> b) -> a -> b
$ \Handle
h -> do
    let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
    let varInfo :: CollectedVarInfo t
varInfo = forall t. Expr t BaseBoolType -> CollectedVarInfo t
predicateVarInfo BoolExpr t
p
    -- check whether to use ef-solve
    let features :: ProblemFeatures
features = CollectedVarInfo t
varInfoforall s a. s -> Getting a s a -> a
^.forall t. Simple Lens (CollectedVarInfo t) ProblemFeatures
problemFeatures
    let efSolver :: Bool
efSolver = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useExistForall

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

    OutputStream Text
str <- OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
h
    InputStream Text
in_str <- forall a. IO (InputStream a)
Streams.nullInput
    let t :: SolverGoalTimeout
t = Integer -> SolverGoalTimeout
SolverGoalTimeout Integer
0  -- no timeout needed; not doing actual solving
    WriterConn t Connection
c <- forall t.
OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
newConnection OutputStream Text
str InputStream Text
in_str (forall a b. a -> b -> a
const forall t h. AcknowledgementAction t h
nullAcknowledgementAction) ProblemFeatures
features SolverGoalTimeout
t SymbolVarBimap t
bindings
    forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
c Config
cfg
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn t Connection
c BoolExpr t
p
    if Bool
efSolver then
      forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c Command Connection
efSolveCommand
    else
      forall t. WriterConn t Connection -> IO ()
sendCheck WriterConn t Connection
c
    forall t. WriterConn t Connection -> IO ()
sendShowModel WriterConn t Connection
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 = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
  [Char]
yices_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
findSolverPath ConfigOption (BaseStringType Unicode)
yicesPath Config
cfg
  BoolExpr t
condition <- forall sym s.
IsExprBuilder sym =>
sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
andAllOf ExprBuilder t st fs
sym forall (f :: Type -> Type) a. Foldable f => IndexedFold Int (f a) a
folded [BoolExpr t]
conditions

  LogData -> Int -> [Char] -> IO ()
logCallbackVerbose LogData
logData Int
2 [Char]
"Calling Yices to check sat"
  -- Check Problem features
  forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
    (SolverStartSATQuery -> SolverEvent
SolverStartSATQuery forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec
    { satQuerySolverName :: [Char]
satQuerySolverName = [Char]
"Yices"
    , satQueryReason :: [Char]
satQueryReason = LogData -> [Char]
logReason LogData
logData
    })
  ProblemFeatures
features <- forall t. BoolExpr t -> IO ProblemFeatures
checkSupportedByYices BoolExpr t
condition
  Bool
enableMCSat <- forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableMCSat Config
cfg
  SolverGoalTimeout
goalTimeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
yicesGoalTimeout Config
cfg)
  let efSolver :: Bool
efSolver = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useExistForall
  let nlSolver :: Bool
nlSolver = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useNonlinearArithmetic
  let args0 :: [[Char]]
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]]
args = [[Char]]
args0 forall a. [a] -> [a] -> [a]
++ if Bool
enableMCSat then [[Char]
"--mcsat"] else []
      hasNamedAssumptions :: Bool
hasNamedAssumptions = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores Bool -> Bool -> Bool
||
                            ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatAssumptions
  forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
enableMCSat Bool -> Bool -> Bool
&& Bool
hasNamedAssumptions) forall a b. (a -> b) -> a -> b
$
     forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Unsat cores and named assumptions are incompatible with MC-SAT in Yices."

  forall a.
[Char]
-> [[Char]]
-> Maybe [Char]
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
withProcessHandles [Char]
yices_path [[Char]]
args forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \hdls :: (Handle, Handle, Handle, ProcessHandle)
hdls@(Handle
in_h, Handle
out_h, Handle
err_h, ProcessHandle
ph) -> do

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

      -- Create new connection for sending commands to yices.
      SymbolVarBimap t
bindings <- forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
B.getSymbolVarBimap ExprBuilder t st fs
sym

      WriterConn t Connection
c <- forall t.
OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
newConnection OutputStream Text
in_stream InputStream Text
out_stream (forall a b. a -> b -> a
const forall t h. AcknowledgementAction t h
nullAcknowledgementAction) ProblemFeatures
features SolverGoalTimeout
goalTimeout SymbolVarBimap t
bindings
      -- Write yices parameters.
      forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
c Config
cfg
      -- Assert condition
      forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn t Connection
c BoolExpr t
condition

      LogData -> Int -> [Char] -> IO ()
logCallbackVerbose LogData
logData Int
2 [Char]
"Running check sat"
      if Bool
efSolver then
        forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c Command Connection
efSolveCommand
      else
        forall t. WriterConn t Connection -> IO ()
sendCheck WriterConn t Connection
c

      let yp :: SolverProcess t Connection
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 = forall h t.
SMTReadWriter h =>
WriterConn t h -> InputStream Text -> SMTEvalFunctions h
smtEvalFuns WriterConn t Connection
c InputStream Text
out_stream
                             , solverName :: [Char]
solverName = [Char]
"Yices"
                             , solverLogFn :: SolverEvent -> IO ()
solverLogFn = forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
                             , solverEarlyUnsat :: IORef (Maybe Int)
solverEarlyUnsat = Connection -> IORef (Maybe Int)
yicesEarlyUnsat (forall t h. WriterConn t h -> h
connState WriterConn t Connection
c)
                             , solverSupportsResetAssertions :: Bool
solverSupportsResetAssertions = Bool
True
                             , solverGoalTimeout :: SolverGoalTimeout
solverGoalTimeout = SolverGoalTimeout
goalTimeout
                             }
      SatResult () ()
sat_result <- forall s t.
SMTReadWriter s =>
SolverProcess t s -> IO (SatResult () ())
getSatResult SolverProcess t Connection
yp
      forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
        (SolverEndSATQuery -> SolverEvent
SolverEndSATQuery forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
        { satQueryResult :: SatResult () ()
satQueryResult = SatResult () ()
sat_result
        , satQueryError :: Maybe [Char]
satQueryError  = forall a. Maybe a
Nothing
        })
      a
r <-
         case SatResult () ()
sat_result of
           Sat () -> SatResult (GroundEvalFn t) () -> IO a
resultFn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall mdl core. mdl -> SatResult mdl core
Sat forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel SolverProcess t Connection
yp
           Unsat ()
x -> SatResult (GroundEvalFn t) () -> IO a
resultFn (forall mdl core. core -> SatResult mdl core
Unsat ()
x)
           SatResult () ()
Unknown -> SatResult (GroundEvalFn t) () -> IO a
resultFn forall mdl core. SatResult mdl core
Unknown

      (ExitCode, Text)
_ <- forall scope. SolverProcess scope Connection -> IO (ExitCode, Text)
yicesShutdownSolver SolverProcess t Connection
yp
      forall (m :: Type -> Type) a. Monad m => a -> m a
return a
r