------------------------------------------------------------------------
-- |
-- 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.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.Config
import           What4.Solver.Adapter
import           What4.Concrete
import           What4.Interface
import           What4.ProblemFeatures
import           What4.SatResult
import qualified What4.Expr.Builder as B
import           What4.Expr.GroundEval
import           What4.Expr.VarIdentification
import           What4.Protocol.SExp
import           What4.Protocol.SMTLib2 (writeDefaultSMT2)
import           What4.Protocol.SMTWriter as SMTWriter
import           What4.Protocol.Online
import qualified What4.Protocol.PolyRoot as Root
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 :: ConcreteVal tp -> Maybe Builder
asYicesConfigValue ConcreteVal tp
v = case ConcreteVal tp
v of
  ConcreteBool Bool
x ->
      Builder -> Maybe Builder
forall (m :: Type -> Type) a. Monad m => a -> m a
return (if Bool
x then Builder
"true" else Builder
"false")
  ConcreteReal Rational
x ->
      Builder -> Maybe Builder
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Integer -> Builder
forall a. Integral a => a -> Builder
decimal (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"/" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Integral a => a -> Builder
decimal (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x)
  ConcreteInteger Integer
x ->
      Builder -> Maybe Builder
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Integer -> Builder
forall a. Integral a => a -> Builder
decimal Integer
x
  ConcreteString (UnicodeLiteral Text
x) ->
      Builder -> Maybe Builder
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
Builder.fromText Text
x
  ConcreteVal tp
_ ->
      Maybe Builder
forall a. Maybe a
Nothing

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

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

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

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

type Expr = YicesTerm

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

yicesType :: TypeMap tp -> YicesType
yicesType :: TypeMap tp -> YicesType
yicesType TypeMap tp
BoolTypeMap    = YicesType
boolType
yicesType TypeMap tp
IntegerTypeMap = YicesType
intType
yicesType TypeMap tp
RealTypeMap    = YicesType
realType
yicesType (BVTypeMap NatRepr w
w)  = Builder -> YicesType
YicesType (Builder -> [Builder] -> Builder
app Builder
"bitvector" [[Char] -> Builder
forall a. IsString a => [Char] -> a
fromString (NatRepr w -> [Char]
forall a. Show a => a -> [Char]
show NatRepr w
w)])
yicesType (FloatTypeMap FloatPrecisionRepr fpp
_) = YicesType
forall a. (?callStack::CallStack) => a
floatFail
yicesType TypeMap tp
Char8TypeMap = YicesType
forall a. (?callStack::CallStack) => a
stringFail
yicesType TypeMap tp
ComplexToStructTypeMap = [YicesType] -> YicesType
tupleType [YicesType
realType, YicesType
realType]
yicesType TypeMap tp
ComplexToArrayTypeMap  = [YicesType] -> YicesType -> YicesType
fnType [YicesType
boolType] YicesType
realType
yicesType (PrimArrayTypeMap Assignment TypeMap (idxl ::> idx)
i TypeMap tp
r) = [YicesType] -> YicesType -> YicesType
fnType ((forall (tp :: BaseType). TypeMap tp -> YicesType)
-> Assignment TypeMap (idxl ::> idx) -> [YicesType]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap (idxl ::> idx)
i) (TypeMap tp -> YicesType
forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType TypeMap tp
r)
yicesType (FnArrayTypeMap Assignment TypeMap (idxl ::> idx)
i TypeMap tp
r)   = [YicesType] -> YicesType -> YicesType
fnType ((forall (tp :: BaseType). TypeMap tp -> YicesType)
-> Assignment TypeMap (idxl ::> idx) -> [YicesType]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap (idxl ::> idx)
i) (TypeMap tp -> YicesType
forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType TypeMap tp
r)
yicesType (StructTypeMap Assignment TypeMap idx
f)      = [YicesType] -> YicesType
tupleType ((forall (tp :: BaseType). TypeMap tp -> YicesType)
-> Assignment TypeMap idx -> [YicesType]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
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 = YicesCommand -> Connection -> YicesCommand
forall a b. a -> b -> a
const (YicesCommand -> Connection -> YicesCommand)
-> YicesCommand -> Connection -> YicesCommand
forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert" [YicesTerm -> Builder
renderTerm YicesTerm
res]
 where res :: YicesTerm
res = Builder -> [Builder] -> YicesTerm -> YicesTerm
binder_app Builder
"forall" ((Text -> YicesType -> Builder) -> (Text, YicesType) -> Builder
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> YicesType -> Builder
mkBinding ((Text, YicesType) -> Builder) -> [(Text, YicesType)] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, YicesType)]
vars) YicesTerm
e
       mkBinding :: Text -> YicesType -> Builder
mkBinding Text
nm YicesType
tp = Text -> Builder
Builder.fromText Text
nm Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"::" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> YicesType -> Builder
unType YicesType
tp


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

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

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

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

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

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

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

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


declareUnitType :: WriterConn t Connection -> IO ()
declareUnitType :: WriterConn t Connection -> IO ()
declareUnitType WriterConn t Connection
conn =
  do Bool
done <- IORef Bool -> (Bool -> (Bool, Bool)) -> IO Bool
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef (Connection -> IORef Bool
yicesUnitDeclared (WriterConn t Connection -> Connection
forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn)) (\Bool
x -> (Bool
True, Bool
x))
     Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless Bool
done (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ WriterConn t Connection -> Command Connection -> IO ()
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 :: WriterConn t Connection -> IO ()
resetUnitType WriterConn t Connection
conn =
  IORef Bool -> Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Connection -> IORef Bool
yicesUnitDeclared (WriterConn t Connection -> Connection
forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn)) Bool
False

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

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

  IORef (Maybe Int)
earlyUnsatRef <- Maybe Int -> IO (IORef (Maybe Int))
forall a. a -> IO (IORef a)
newIORef Maybe Int
forall a. Maybe a
Nothing
  IORef Bool
unitRef <- Bool -> IO (IORef Bool)
forall a. a -> IO (IORef a)
newIORef Bool
False
  let c :: Connection
c = Connection :: IORef (Maybe Int) -> SolverGoalTimeout -> IORef Bool -> Connection
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 <- OutputStream Text
-> InputStream Text
-> AcknowledgementAction t Connection
-> [Char]
-> ProblemFeatures
-> SymbolVarBimap t
-> Connection
-> IO (WriterConn t Connection)
forall t cs.
OutputStream Text
-> InputStream Text
-> AcknowledgementAction t cs
-> [Char]
-> 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 ProblemFeatures
features' SymbolVarBimap t
bindings Connection
c
  WriterConn t Connection -> IO (WriterConn t Connection)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (WriterConn t Connection -> IO (WriterConn t Connection))
-> WriterConn t Connection -> IO (WriterConn t Connection)
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 :: Bool -> Builder -> YicesCommand
YicesCommand { cmdEarlyUnsatSafe :: Bool
cmdEarlyUnsatSafe = Bool
True, cmdCmd :: Builder
cmdCmd = Builder
txt }

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

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

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

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

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

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

  getUnsatAssumptionsCommand :: f Connection -> Command Connection
getUnsatAssumptionsCommand f Connection
_ = YicesCommand -> Connection -> YicesCommand
forall a b. a -> b -> a
const (YicesCommand -> Connection -> YicesCommand)
-> YicesCommand -> Connection -> YicesCommand
forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(show-unsat-assumptions)"
  getUnsatCoreCommand :: f Connection -> Command Connection
getUnsatCoreCommand f Connection
_ = YicesCommand -> Connection -> YicesCommand
forall a b. a -> b -> a
const (YicesCommand -> Connection -> YicesCommand)
-> YicesCommand -> Connection -> YicesCommand
forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(show-unsat-core)"
  setOptCommand :: 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 :: f Connection -> Term Connection -> Command Connection
assertCommand f Connection
_ (T nm) = YicesCommand -> Connection -> YicesCommand
forall a b. a -> b -> a
const (YicesCommand -> Connection -> YicesCommand)
-> YicesCommand -> Connection -> YicesCommand
forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert" [Builder
nm]
  assertNamedCommand :: f Connection -> Term Connection -> Text -> Command Connection
assertNamedCommand f Connection
_ (T tm) Text
nm = YicesCommand -> Connection -> YicesCommand
forall a b. a -> b -> a
const (YicesCommand -> Connection -> YicesCommand)
-> YicesCommand -> Connection -> YicesCommand
forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd (Builder -> YicesCommand) -> Builder -> YicesCommand
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert" [Builder
tm, Text -> Builder
Builder.fromText Text
nm]

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

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

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

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

  structCtor :: Assignment TypeMap args -> [Term Connection] -> Term Connection
structCtor Assignment TypeMap args
_tps []   = Builder -> YicesTerm
T Builder
"unit-value"
  structCtor Assignment TypeMap args
_tps [Term Connection]
args = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"mk-tuple" [Term Connection]
[YicesTerm]
args

  stringTerm :: ByteString -> Term Connection
stringTerm ByteString
_   = Term Connection
forall a. (?callStack::CallStack) => a
stringFail
  stringLength :: Term Connection -> Term Connection
stringLength Term Connection
_ = Term Connection
forall a. (?callStack::CallStack) => a
stringFail
  stringAppend :: [Term Connection] -> Term Connection
stringAppend [Term Connection]
_ = Term Connection
forall a. (?callStack::CallStack) => a
stringFail
  stringContains :: Term Connection -> Term Connection -> Term Connection
stringContains Term Connection
_ 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
_ = Term Connection
forall a. (?callStack::CallStack) => a
stringFail
  stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection
stringIsPrefixOf Term Connection
_ Term Connection
_ = Term Connection
forall a. (?callStack::CallStack) => a
stringFail
  stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection
stringIsSuffixOf Term Connection
_ 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
_ = 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 :: WriterConn t Connection -> Assignment TypeMap args -> IO ()
declareStructDatatype WriterConn t Connection
conn Assignment TypeMap args
Ctx.Empty = WriterConn t Connection -> IO ()
forall t. WriterConn t Connection -> IO ()
declareUnitType WriterConn t Connection
conn
  declareStructDatatype WriterConn t Connection
_ Assignment TypeMap args
_ = () -> IO ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

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

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

  smtSatResult :: f Connection -> InputStream Text -> IO (SatResult () ())
smtSatResult f Connection
_ = InputStream Text -> IO (SatResult () ())
getSatResponse

  smtUnsatAssumptionsResult :: f Connection -> InputStream Text -> IO [(Bool, Text)]
smtUnsatAssumptionsResult f Connection
_ InputStream Text
s =
    do Either SomeException SExp
mb <- (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) InputStream Text
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) -> [(Bool, Text)] -> IO [(Bool, Text)]
forall (m :: Type -> Type) a. Monad m => a -> m a
return [(Bool, Text)]
as
         Right (SApp [SAtom Text
"error", SString Text
msg]) -> YicesException -> IO [(Bool, Text)]
forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesError YicesCommand
cmd Text
msg)
         Right SExp
res -> YicesException -> IO [(Bool, Text)]
forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd ([Char] -> Text
Text.pack (SExp -> [Char]
forall a. Show a => a -> [Char]
show SExp
res)))
         Left (SomeException e
e) -> YicesException -> IO [(Bool, Text)]
forall a e. Exception e => e -> a
throw (YicesException -> IO [(Bool, Text)])
-> YicesException -> IO [(Bool, Text)]
forall a b. (a -> b) -> a -> b
$ YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd (Text -> YicesException) -> Text -> YicesException
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
Text.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$
                 [[Char]] -> [Char]
unlines [ [Char]
"Could not parse unsat assumptions result."
                         , [Char]
"*** Exception: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ e -> [Char]
forall e. Exception e => e -> [Char]
displayException e
e
                         ]

  smtUnsatCoreResult :: f Connection -> InputStream Text -> IO [Text]
smtUnsatCoreResult f Connection
_ InputStream Text
s =
    do Either SomeException SExp
mb <- (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) InputStream Text
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) -> [Text] -> IO [Text]
forall (m :: Type -> Type) a. Monad m => a -> m a
return [Text]
nms

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


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

instance Show YicesException where
  show :: YicesException -> [Char]
show (YicesUnsupported (YicesCommand Bool
_ Builder
cmd)) =
     [[Char]] -> [Char]
unlines
       [ [Char]
"unsupported command:"
       , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ 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]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack Text
msg
       , [Char]
"in response to command:"
       , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ 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]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack Text
msg
       , [Char]
"in response to command:"
       , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)
       ]

instance Exception YicesException

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

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

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

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


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

yicesStartSolver ::
  ProblemFeatures ->
  Maybe Handle ->
  B.ExprBuilder t st fs ->
  IO (SolverProcess t Connection)
yicesStartSolver :: ProblemFeatures
-> Maybe Handle
-> ExprBuilder t st fs
-> IO (SolverProcess t Connection)
yicesStartSolver ProblemFeatures
features Maybe Handle
auxOutput ExprBuilder t st fs
sym = do -- FIXME
  let cfg :: Config
cfg = ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
  [Char]
yices_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
findSolverPath ConfigOption (BaseStringType Unicode)
yicesPath Config
cfg
  Bool
enableMCSat <- OptionSetting BaseBoolType -> IO Bool
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseBoolType -> IO Bool)
-> IO (OptionSetting BaseBoolType) -> IO Bool
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableMCSat Config
cfg
  Bool
enableInteractive <- OptionSetting BaseBoolType -> IO Bool
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseBoolType -> IO Bool)
-> IO (OptionSetting BaseBoolType) -> IO Bool
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableInteractive Config
cfg
  SolverGoalTimeout
goalTimeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout (Integer -> SolverGoalTimeout)
-> (Integer -> Integer) -> Integer -> SolverGoalTimeout
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
1000Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*) (Integer -> SolverGoalTimeout)
-> IO Integer -> IO SolverGoalTimeout
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseIntegerType -> IO Integer)
-> IO (OptionSetting BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
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) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 = [Char]
"--mode=interactive"
               | Bool
otherwise = [Char]
"--mode=push-pop"
      args :: [[Char]]
args = [Char]
modeFlag [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [Char]
"--print-success" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
             if Bool
enableMCSat then [[Char]
"--mcsat"] else []
      hasNamedAssumptions :: Bool
hasNamedAssumptions = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores Bool -> Bool -> Bool
||
                            ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatAssumptions
  Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
enableMCSat Bool -> Bool -> Bool
&& Bool
hasNamedAssumptions) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
     [Char] -> IO ()
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Unsat cores and named assumptions are incompatible with MC-SAT in Yices."

  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 Maybe [Char]
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
      ((Handle -> (Text, Handle)) -> Maybe Handle -> Maybe (Text, Handle)
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' <- IO () -> OutputStream Text -> IO (OutputStream Text)
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 <- OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
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 IORef (Maybe Int) -> AcknowledgementAction t Connection
forall s. IORef (Maybe Int) -> AcknowledgementAction s Connection
yicesAck ProblemFeatures
features SolverGoalTimeout
goalTimeout SymbolVarBimap t
forall t. SymbolVarBimap t
B.emptySymbolVarBimap

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

  SolverProcess t Connection -> IO (SolverProcess t Connection)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SolverProcess t Connection -> IO (SolverProcess t Connection))
-> SolverProcess t Connection -> IO (SolverProcess t Connection)
forall a b. (a -> b) -> a -> b
$! SolverProcess :: forall scope solver.
WriterConn scope solver
-> IO ExitCode
-> ProcessHandle
-> OutputStream Text
-> InputStream Text
-> ErrorBehavior
-> HandleReader
-> SMTEvalFunctions solver
-> (SolverEvent -> IO ())
-> [Char]
-> IORef (Maybe Int)
-> Bool
-> SolverGoalTimeout
-> SolverProcess scope solver
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
                          , solverStdin :: OutputStream Text
solverStdin  = OutputStream Text
in_stream'
                          , solverStderr :: HandleReader
solverStderr = HandleReader
err_reader
                          , solverHandle :: ProcessHandle
solverHandle = ProcessHandle
ph
                          , solverResponse :: InputStream Text
solverResponse = InputStream Text
out_stream
                          , solverErrorBehavior :: ErrorBehavior
solverErrorBehavior = ErrorBehavior
ContinueOnError
                          , solverEvalFuns :: SMTEvalFunctions Connection
solverEvalFuns = WriterConn t Connection
-> InputStream Text -> SMTEvalFunctions Connection
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 = ExprBuilder t st fs -> SolverEvent -> IO ()
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 (WriterConn t Connection -> Connection
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 :: WriterConn t Connection -> IO ()
sendCheck WriterConn t Connection
c = WriterConn t Connection -> [Command Connection] -> IO ()
forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn t Connection
c (WriterConn t Connection -> [Command Connection]
forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands WriterConn t Connection
c)

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

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

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

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

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

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






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

-- | Get the sat result from a previous SAT command.
-- Throws an exception if something goes wrong.
getSatResponse :: Streams.InputStream Text -> IO (SatResult () ())
getSatResponse :: InputStream Text -> IO (SatResult () ())
getSatResponse InputStream Text
resps =
  do Either SomeException SExp
mb <- (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) InputStream Text
resps)
     case Either SomeException SExp
mb of
       Right (SAtom Text
"unsat")   -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (() -> SatResult () ()
forall mdl core. core -> SatResult mdl core
Unsat ())
       Right (SAtom Text
"sat")     -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (() -> SatResult () ()
forall mdl core. mdl -> SatResult mdl core
Sat ())
       Right (SAtom Text
"unknown") -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult () ()
forall mdl core. SatResult mdl core
Unknown
       Right (SAtom Text
"interrupted") -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult () ()
forall mdl core. SatResult mdl core
Unknown
       Right SExp
res -> [Char] -> IO (SatResult () ())
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO (SatResult () ())) -> [Char] -> IO (SatResult () ())
forall a b. (a -> b) -> a -> b
$
               [[Char]] -> [Char]
unlines [ [Char]
"Could not parse sat result."
                       , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SExp -> [Char]
forall a. Show a => a -> [Char]
show SExp
res
                       ]
       Left (SomeException e
e) -> [Char] -> IO (SatResult () ())
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO (SatResult () ())) -> [Char] -> IO (SatResult () ())
forall a b. (a -> b) -> a -> b
$
               [[Char]] -> [Char]
unlines [ [Char]
"Could not parse sat result."
                       , [Char]
"*** Exception: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ e -> [Char]
forall e. Exception e => e -> [Char]
displayException e
e
                       ]

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

parseYicesString :: Atto.Parser Text
parseYicesString :: Parser Text
parseYicesString = Char -> Parser Char
Atto.char Char
'\"' Parser Char -> Parser Text -> Parser Text
forall (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 <- [Parser Text [Char]] -> Parser Text [Char]
forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
Atto.choice [ Int -> Parser Char -> Parser Text [Char]
forall (m :: Type -> Type) a. Monad m => Int -> m a -> m [a]
Atto.count Int
i Parser Char
octalDigit | Int
i <- [ Int
3, Int
2, Int
1] ]
      case ReadS Int
forall a. (Eq a, Num a) => ReadS a
readOct [Char]
ds of
        (Int
c,[Char]
""):[(Int, [Char])]
_ -> Text -> Parser Text
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Char -> Text
Text.singleton (Int -> Char
forall a. Enum a => Int -> a
toEnum Int
c))
        [(Int, [Char])]
_ -> Parser Text
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero

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

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

boolValue :: Atto.Parser Bool
boolValue :: Parser Bool
boolValue =
  [Parser Bool] -> Parser Bool
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
  [ Text -> Parser Text
Atto.string Text
"true" Parser Text -> Parser Bool -> Parser Bool
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Bool -> Parser Bool
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
  , Text -> Parser Text
Atto.string Text
"false" Parser Text -> Parser Bool -> Parser Bool
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Bool -> Parser Bool
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 :: Eval s Bool
yicesEvalBool WriterConn s Connection
conn InputStream Text
resp Term Connection
tm =
  do WriterConn s Connection -> Term Connection -> IO ()
forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn s Connection
conn Term Connection
tm
     Either SomeException Bool
mb <- (SomeException -> Maybe SomeException)
-> IO Bool -> IO (Either SomeException Bool)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser Bool -> InputStream Text -> IO Bool
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser ()
skipSpaceOrNewline Parser () -> Parser Bool -> Parser Bool
forall (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) ->
           [Char] -> IO Bool
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO Bool) -> [Char] -> IO Bool
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
             [ [Char]
"Could not parse boolean value returned by yices: "
             , e -> [Char]
forall e. Exception e => e -> [Char]
displayException e
ex
             ]
       Right Bool
b -> Bool -> IO Bool
forall (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 (Char -> [Char] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` ([Char]
"01"::String))
     Int -> [Char] -> Parser Integer
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 :: NatRepr w -> Eval s (BV w)
yicesEvalBV NatRepr w
w WriterConn s Connection
conn InputStream Text
resp Term Connection
tm =
  do WriterConn s Connection -> Term Connection -> IO ()
forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn s Connection
conn Term Connection
tm
     Either SomeException Integer
mb <- (SomeException -> Maybe SomeException)
-> IO Integer -> IO (Either SomeException Integer)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser Integer -> InputStream Text -> IO Integer
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser ()
skipSpaceOrNewline Parser () -> Parser Integer -> Parser Integer
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Int -> Parser Integer
yicesBV (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w)) InputStream Text
resp)
     case Either SomeException Integer
mb of
       Left (SomeException e
ex) ->
           [Char] -> IO (BV w)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO (BV w)) -> [Char] -> IO (BV w)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
             [ [Char]
"Could not parse bitvector value returned by yices: "
             , e -> [Char]
forall e. Exception e => e -> [Char]
displayException e
ex
             ]
       Right Integer
b -> BV w -> IO (BV w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
b)

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

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

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

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

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

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

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

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

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

yicesOptions :: [ConfigDesc]
yicesOptions :: [ConfigDesc]
yicesOptions =
  [ ConfigOption (BaseStringType Unicode)
-> OptionStyle (BaseStringType Unicode)
-> Maybe (Doc Void)
-> Maybe (ConcreteVal (BaseStringType Unicode))
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
      ConfigOption (BaseStringType Unicode)
yicesPath
      OptionStyle (BaseStringType Unicode)
executablePathOptSty
      (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Yices executable path")
      (ConcreteVal (BaseStringType Unicode)
-> Maybe (ConcreteVal (BaseStringType Unicode))
forall a. a -> Maybe a
Just (StringLiteral Unicode -> ConcreteVal (BaseStringType Unicode)
forall (si :: StringInfo).
StringLiteral si -> ConcreteVal (BaseStringType si)
ConcreteString StringLiteral Unicode
"yices"))
  , ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
      ConfigOption BaseBoolType
yicesEnableMCSat
      OptionStyle BaseBoolType
boolOptSty
      (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Enable the Yices MCSAT solving engine")
      (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))
  , ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
      ConfigOption BaseBoolType
yicesEnableInteractive
      OptionStyle BaseBoolType
boolOptSty
      (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Enable Yices interactive mode (needed to support timeouts)")
      (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))
  , ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
      ConfigOption BaseIntegerType
yicesGoalTimeout
      OptionStyle BaseIntegerType
integerOptSty
      (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Set a per-goal timeout")
      (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
0))
  ]
  [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
forall a. [a] -> [a] -> [a]
++ [ConfigDesc]
yicesInternalOptions

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

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

booleanOpt :: String -> ConfigDesc
booleanOpt :: [Char] -> ConfigDesc
booleanOpt [Char]
nm = ConfigOption BaseBoolType -> ConfigDesc
booleanOpt' (BaseTypeRepr BaseBoolType -> [Char] -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
BaseBoolRepr ([Char]
"yices."[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
nm))

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

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

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

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

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

yicesInternalOptions :: [ConfigDesc]
yicesInternalOptions :: [ConfigDesc]
yicesInternalOptions =
  [ [Char] -> ConfigDesc
booleanOpt [Char]
"var-elim"
  , [Char] -> ConfigDesc
booleanOpt [Char]
"arith-elim"
  , [Char] -> ConfigDesc
booleanOpt [Char]
"flatten"
  , [Char] -> ConfigDesc
booleanOpt [Char]
"learn-eq"
  , [Char] -> ConfigDesc
booleanOpt [Char]
"keep-ite"
  , [Char] -> ConfigDesc
booleanOpt [Char]
"fast-restarts"

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

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

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

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

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

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

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

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

    OutputStream Text
str <- OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 (OutputStream ByteString -> IO (OutputStream Text))
-> IO (OutputStream ByteString) -> IO (OutputStream Text)
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 <- IO (InputStream Text)
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 <- OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
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 (AcknowledgementAction t Connection
-> IORef (Maybe Int) -> AcknowledgementAction t Connection
forall a b. a -> b -> a
const AcknowledgementAction t Connection
forall t h. AcknowledgementAction t h
nullAcknowledgementAction) ProblemFeatures
features SolverGoalTimeout
t SymbolVarBimap t
bindings
    WriterConn t Connection -> Config -> IO ()
forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
c Config
cfg
    WriterConn t Connection -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn t Connection
c BoolExpr t
p
    if Bool
efSolver then
      WriterConn t Connection -> Command Connection -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c Command Connection
efSolveCommand
    else
      WriterConn t Connection -> IO ()
forall t. WriterConn t Connection -> IO ()
sendCheck WriterConn t Connection
c
    WriterConn t Connection -> IO ()
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 :: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t) () -> IO a)
-> IO a
runYicesInOverride ExprBuilder t st fs
sym LogData
logData [BoolExpr t]
conditions SatResult (GroundEvalFn t) () -> IO a
resultFn = do
  let cfg :: Config
cfg = ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
  [Char]
yices_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
findSolverPath ConfigOption (BaseStringType Unicode)
yicesPath Config
cfg
  BoolExpr t
condition <- ExprBuilder t st fs
-> Fold [BoolExpr t] (Pred (ExprBuilder t st fs))
-> [BoolExpr t]
-> IO (Pred (ExprBuilder t st fs))
forall sym s.
IsExprBuilder sym =>
sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
andAllOf ExprBuilder t st fs
sym Fold [BoolExpr t] (Pred (ExprBuilder t st fs))
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
  ExprBuilder t st fs -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
    SolverStartSATQuery :: [Char] -> [Char] -> SolverEvent
SolverStartSATQuery
    { satQuerySolverName :: [Char]
satQuerySolverName = [Char]
"Yices"
    , satQueryReason :: [Char]
satQueryReason = LogData -> [Char]
logReason LogData
logData
    }
  ProblemFeatures
features <- BoolExpr t -> IO ProblemFeatures
forall t. BoolExpr t -> IO ProblemFeatures
checkSupportedByYices BoolExpr t
condition
  Bool
enableMCSat <- OptionSetting BaseBoolType -> IO Bool
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseBoolType -> IO Bool)
-> IO (OptionSetting BaseBoolType) -> IO Bool
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableMCSat Config
cfg
  SolverGoalTimeout
goalTimeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout (Integer -> SolverGoalTimeout)
-> IO Integer -> IO SolverGoalTimeout
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseIntegerType -> IO Integer)
-> IO (OptionSetting BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
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 [[Char]] -> [[Char]] -> [[Char]]
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
  Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
enableMCSat Bool -> Bool -> Bool
&& Bool
hasNamedAssumptions) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
     [Char] -> IO ()
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Unsat cores and named assumptions are incompatible with MC-SAT in Yices."

  [Char]
-> [[Char]]
-> Maybe [Char]
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
forall a.
[Char]
-> [[Char]]
-> Maybe [Char]
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
withProcessHandles [Char]
yices_path [[Char]]
args Maybe [Char]
forall a. Maybe a
Nothing (((Handle, Handle, Handle, ProcessHandle) -> IO a) -> IO a)
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a) -> IO a
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
          ((Handle -> (Text, Handle)) -> Maybe Handle -> Maybe (Text, Handle)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Handle
x -> (Text
"; ",Handle
x)) (Maybe Handle -> Maybe (Text, Handle))
-> Maybe Handle -> Maybe (Text, Handle)
forall a b. (a -> b) -> a -> b
$ LogData -> Maybe Handle
logHandle LogData
logData)

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

      WriterConn t Connection
c <- OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
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 (AcknowledgementAction t Connection
-> IORef (Maybe Int) -> AcknowledgementAction t Connection
forall a b. a -> b -> a
const AcknowledgementAction t Connection
forall t h. AcknowledgementAction t h
nullAcknowledgementAction) ProblemFeatures
features SolverGoalTimeout
goalTimeout SymbolVarBimap t
bindings
      -- Write yices parameters.
      WriterConn t Connection -> Config -> IO ()
forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
c Config
cfg
      -- Assert condition
      WriterConn t Connection -> BoolExpr t -> IO ()
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
        WriterConn t Connection -> Command Connection -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c Command Connection
efSolveCommand
      else
        WriterConn t Connection -> IO ()
forall t. WriterConn t Connection -> IO ()
sendCheck WriterConn t Connection
c

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

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