{-# 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
(
Connection
, newConnection
, SMTWriter.assume
, sendCheck
, sendCheckExistsForall
, eval
, push
, pop
, inNewFrame
, setParam
, setYicesParams
, HandleReader
, startHandleReader
, yicesType
, assertForall
, efSolveCommand
, YicesException(..)
, yicesEvalBool
, SMTWriter.addCommand
, yicesAdapter
, runYicesInOverride
, writeYicesFile
, yicesPath
, yicesOptions
, yicesDefaultFeatures
, yicesEnableMCSat
, yicesEnableInteractive
, yicesGoalTimeout
) where
#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail ( MonadFail )
#endif
import Control.Applicative
import Control.Concurrent ( threadDelay )
import Control.Concurrent.Async ( race )
import Control.Exception
(assert, SomeException(..), tryJust, throw, displayException, Exception(..))
import Control.Lens ((^.), folded)
import Control.Monad
import Control.Monad.Identity
import qualified Data.Attoparsec.Text as Atto
import Data.Bits
import qualified Data.BitVector.Sized as BV
import Data.IORef
import Data.Foldable (toList)
import Data.Maybe
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (fromString)
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Text.Lazy as Lazy
import Data.Text.Lazy.Builder (Builder)
import qualified Data.Text.Lazy.Builder as Builder
import Data.Text.Lazy.Builder.Int (decimal)
import Numeric (readOct)
import System.Exit
import System.IO
import qualified System.IO.Streams as Streams
import qualified System.IO.Streams.Attoparsec.Text as Streams
import qualified Prettyprinter as PP
import What4.BaseTypes
import What4.Concrete
import What4.Config
import qualified What4.Expr.Builder as B
import What4.Expr.GroundEval
import What4.Expr.VarIdentification
import What4.Interface
import What4.ProblemFeatures
import What4.Protocol.Online
import qualified What4.Protocol.PolyRoot as Root
import What4.Protocol.SExp
import What4.Protocol.SMTLib2 (writeDefaultSMT2)
import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
import What4.Protocol.SMTWriter as SMTWriter
import What4.SatResult
import What4.Solver.Adapter
import What4.Utils.HandleReader
import What4.Utils.Process
import Prelude
import GHC.Stack
data Connection = Connection
{ Connection -> IORef (Maybe Int)
yicesEarlyUnsat :: IORef (Maybe Int)
, Connection -> SolverGoalTimeout
yicesTimeout :: SolverGoalTimeout
, Connection -> IORef Bool
yicesUnitDeclared :: IORef Bool
}
asYicesConfigValue :: ConcreteVal tp -> Maybe Builder
asYicesConfigValue :: forall (tp :: BaseType). ConcreteVal tp -> Maybe Builder
asYicesConfigValue ConcreteVal tp
v = case ConcreteVal tp
v of
ConcreteBool Bool
x ->
forall (m :: Type -> Type) a. Monad m => a -> m a
return (if Bool
x then Builder
"true" else Builder
"false")
ConcreteReal Rational
x ->
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
decimal (forall a. Ratio a -> a
numerator Rational
x) forall a. Semigroup a => a -> a -> a
<> Builder
"/" forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
decimal (forall a. Ratio a -> a
denominator Rational
x)
ConcreteInteger Integer
x ->
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
decimal Integer
x
ConcreteString (UnicodeLiteral Text
x) ->
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Text -> Builder
Builder.fromText Text
x
ConcreteVal tp
_ ->
forall a. Maybe a
Nothing
newtype YicesTerm = T { YicesTerm -> Builder
renderTerm :: Builder }
term_app :: Builder -> [YicesTerm] -> YicesTerm
term_app :: Builder -> [YicesTerm] -> YicesTerm
term_app Builder
o [YicesTerm]
args = Builder -> YicesTerm
T (Builder -> [Builder] -> Builder
app Builder
o (YicesTerm -> Builder
renderTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [YicesTerm]
args))
bin_app :: Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app :: Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
o YicesTerm
x YicesTerm
y = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
o [YicesTerm
x,YicesTerm
y]
type Expr = YicesTerm
instance Num YicesTerm where
+ :: YicesTerm -> YicesTerm -> YicesTerm
(+) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"+"
(-) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"-"
* :: YicesTerm -> YicesTerm -> YicesTerm
(*) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"*"
negate :: YicesTerm -> YicesTerm
negate YicesTerm
x = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"-" [YicesTerm
x]
abs :: YicesTerm -> YicesTerm
abs YicesTerm
x = forall v. SupportTermOps v => v -> v -> v -> v
ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
">=" YicesTerm
x YicesTerm
0) YicesTerm
x (forall a. Num a => a -> a
negate YicesTerm
x)
signum :: YicesTerm -> YicesTerm
signum YicesTerm
x = forall v. SupportTermOps v => v -> v -> v -> v
ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"=" YicesTerm
x YicesTerm
0) YicesTerm
0 forall a b. (a -> b) -> a -> b
$ forall v. SupportTermOps v => v -> v -> v -> v
ite (Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
">" YicesTerm
x YicesTerm
0) YicesTerm
1 (forall a. Num a => a -> a
negate YicesTerm
1)
fromInteger :: Integer -> YicesTerm
fromInteger Integer
i = Builder -> YicesTerm
T (forall a. Integral a => a -> Builder
decimal Integer
i)
decimal_term :: Integral a => a -> YicesTerm
decimal_term :: forall a. Integral a => a -> YicesTerm
decimal_term a
i = Builder -> YicesTerm
T (forall a. Integral a => a -> Builder
decimal a
i)
width_term :: NatRepr n -> YicesTerm
width_term :: forall (n :: Nat). NatRepr n -> YicesTerm
width_term NatRepr n
w = forall a. Integral a => a -> YicesTerm
decimal_term (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr n
w)
varBinding :: Text -> Some TypeMap -> Builder
varBinding :: Text -> Some TypeMap -> Builder
varBinding Text
nm Some TypeMap
tp = Text -> Builder
Builder.fromText Text
nm forall a. Semigroup a => a -> a -> a
<> Builder
"::" forall a. Semigroup a => a -> a -> a
<> YicesType -> Builder
unType (forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Some TypeMap
tp)
letBinding :: Text -> YicesTerm -> Builder
letBinding :: Text -> YicesTerm -> Builder
letBinding Text
nm YicesTerm
t = Builder -> [Builder] -> Builder
app (Text -> Builder
Builder.fromText Text
nm) [YicesTerm -> Builder
renderTerm YicesTerm
t]
binder_app :: Builder -> [Builder] -> YicesTerm -> YicesTerm
binder_app :: Builder -> [Builder] -> YicesTerm -> YicesTerm
binder_app Builder
_ [] YicesTerm
t = YicesTerm
t
binder_app Builder
nm (Builder
h:[Builder]
r) YicesTerm
t = Builder -> YicesTerm
T (Builder -> [Builder] -> Builder
app Builder
nm [Builder -> [Builder] -> Builder
app_list Builder
h [Builder]
r, YicesTerm -> Builder
renderTerm YicesTerm
t])
yicesLambda :: [(Text, Some TypeMap)] -> YicesTerm -> YicesTerm
yicesLambda :: [(Text, Some TypeMap)] -> YicesTerm -> YicesTerm
yicesLambda [] YicesTerm
t = YicesTerm
t
yicesLambda [(Text, Some TypeMap)]
args YicesTerm
t = Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"lambda" [ [Builder] -> Builder
builder_list (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Some TypeMap -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
args), YicesTerm -> Builder
renderTerm YicesTerm
t ]
instance SupportTermOps YicesTerm where
boolExpr :: Bool -> YicesTerm
boolExpr Bool
b = Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ if Bool
b then Builder
"true" else Builder
"false"
notExpr :: YicesTerm -> YicesTerm
notExpr YicesTerm
x = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"not" [YicesTerm
x]
andAll :: [YicesTerm] -> YicesTerm
andAll [] = Builder -> YicesTerm
T Builder
"true"
andAll [YicesTerm
x] = YicesTerm
x
andAll [YicesTerm]
xs = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"and" [YicesTerm]
xs
orAll :: [YicesTerm] -> YicesTerm
orAll [] = Builder -> YicesTerm
T Builder
"false"
orAll [YicesTerm
x] = YicesTerm
x
orAll [YicesTerm]
xs = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"or" [YicesTerm]
xs
.== :: YicesTerm -> YicesTerm -> YicesTerm
(.==) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"="
./= :: YicesTerm -> YicesTerm -> YicesTerm
(./=) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"/="
ite :: YicesTerm -> YicesTerm -> YicesTerm -> YicesTerm
ite YicesTerm
c YicesTerm
x YicesTerm
y = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"if" [YicesTerm
c, YicesTerm
x, YicesTerm
y]
letExpr :: [(Text, YicesTerm)] -> YicesTerm -> YicesTerm
letExpr [(Text, YicesTerm)]
vars YicesTerm
t = Builder -> [Builder] -> YicesTerm -> YicesTerm
binder_app Builder
"let" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> YicesTerm -> Builder
letBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, YicesTerm)]
vars) YicesTerm
t
sumExpr :: [YicesTerm] -> YicesTerm
sumExpr [] = YicesTerm
0
sumExpr [YicesTerm
e] = YicesTerm
e
sumExpr [YicesTerm]
l = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"+" [YicesTerm]
l
termIntegerToReal :: YicesTerm -> YicesTerm
termIntegerToReal = forall a. a -> a
id
termRealToInteger :: YicesTerm -> YicesTerm
termRealToInteger = forall a. a -> a
id
integerTerm :: Integer -> YicesTerm
integerTerm Integer
i = Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
decimal Integer
i
intDiv :: YicesTerm -> YicesTerm -> YicesTerm
intDiv YicesTerm
x YicesTerm
y = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"div" [YicesTerm
x,YicesTerm
y]
intMod :: YicesTerm -> YicesTerm -> YicesTerm
intMod YicesTerm
x YicesTerm
y = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"mod" [YicesTerm
x,YicesTerm
y]
intAbs :: YicesTerm -> YicesTerm
intAbs YicesTerm
x = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"abs" [YicesTerm
x]
intDivisible :: YicesTerm -> Nat -> YicesTerm
intDivisible YicesTerm
x Nat
0 = YicesTerm
x forall v. SupportTermOps v => v -> v -> v
.== forall v. SupportTermOps v => Integer -> v
integerTerm Integer
0
intDivisible YicesTerm
x Nat
k = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"divides" [forall v. SupportTermOps v => Integer -> v
integerTerm (forall a. Integral a => a -> Integer
toInteger Nat
k), YicesTerm
x]
rationalTerm :: Rational -> YicesTerm
rationalTerm Rational
r | Integer
d forall a. Eq a => a -> a -> Bool
== Integer
1 = Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
decimal Integer
n
| Bool
otherwise = Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"/" [forall a. Integral a => a -> Builder
decimal Integer
n, forall a. Integral a => a -> Builder
decimal Integer
d]
where n :: Integer
n = forall a. Ratio a -> a
numerator Rational
r
d :: Integer
d = forall a. Ratio a -> a
denominator Rational
r
.< :: YicesTerm -> YicesTerm -> YicesTerm
(.<) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"<"
.<= :: YicesTerm -> YicesTerm -> YicesTerm
(.<=) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"<="
.> :: YicesTerm -> YicesTerm -> YicesTerm
(.>) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
">"
.>= :: YicesTerm -> YicesTerm -> YicesTerm
(.>=) = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
">="
bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> YicesTerm
bvTerm NatRepr w
w BV w
u = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"mk-bv" [forall (n :: Nat). NatRepr n -> YicesTerm
width_term NatRepr w
w, forall a. Integral a => a -> YicesTerm
decimal_term Integer
d]
where d :: Integer
d = forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
u
bvNeg :: YicesTerm -> YicesTerm
bvNeg YicesTerm
x = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"bv-neg" [YicesTerm
x]
bvAdd :: YicesTerm -> YicesTerm -> YicesTerm
bvAdd = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-add"
bvSub :: YicesTerm -> YicesTerm -> YicesTerm
bvSub = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-sub"
bvMul :: YicesTerm -> YicesTerm -> YicesTerm
bvMul = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-mul"
bvSLe :: YicesTerm -> YicesTerm -> YicesTerm
bvSLe = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-sle"
bvULe :: YicesTerm -> YicesTerm -> YicesTerm
bvULe = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-le"
bvSLt :: YicesTerm -> YicesTerm -> YicesTerm
bvSLt = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-slt"
bvULt :: YicesTerm -> YicesTerm -> YicesTerm
bvULt = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-lt"
bvUDiv :: YicesTerm -> YicesTerm -> YicesTerm
bvUDiv = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-div"
bvURem :: YicesTerm -> YicesTerm -> YicesTerm
bvURem = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-rem"
bvSDiv :: YicesTerm -> YicesTerm -> YicesTerm
bvSDiv = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-sdiv"
bvSRem :: YicesTerm -> YicesTerm -> YicesTerm
bvSRem = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-srem"
bvAnd :: YicesTerm -> YicesTerm -> YicesTerm
bvAnd = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-and"
bvOr :: YicesTerm -> YicesTerm -> YicesTerm
bvOr = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-or"
bvXor :: YicesTerm -> YicesTerm -> YicesTerm
bvXor = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-xor"
bvNot :: YicesTerm -> YicesTerm
bvNot YicesTerm
x = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"bv-not" [YicesTerm
x]
bvShl :: YicesTerm -> YicesTerm -> YicesTerm
bvShl = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-shl"
bvLshr :: YicesTerm -> YicesTerm -> YicesTerm
bvLshr = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-lshr"
bvAshr :: YicesTerm -> YicesTerm -> YicesTerm
bvAshr = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-ashr"
bvConcat :: YicesTerm -> YicesTerm -> YicesTerm
bvConcat YicesTerm
x YicesTerm
y = Builder -> YicesTerm -> YicesTerm -> YicesTerm
bin_app Builder
"bv-concat" YicesTerm
x YicesTerm
y
bvExtract :: forall (w :: Nat).
NatRepr w -> Nat -> Nat -> YicesTerm -> YicesTerm
bvExtract NatRepr w
_ Nat
b Nat
n YicesTerm
x = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Nat
n forall a. Ord a => a -> a -> Bool
> Nat
0) forall a b. (a -> b) -> a -> b
$
let
end :: YicesTerm
end = forall a. Integral a => a -> YicesTerm
decimal_term (Nat
bforall a. Num a => a -> a -> a
+Nat
nforall a. Num a => a -> a -> a
-Nat
1)
begin :: YicesTerm
begin = forall a. Integral a => a -> YicesTerm
decimal_term Nat
b
in Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"bv-extract" [YicesTerm
end, YicesTerm
begin, YicesTerm
x]
realIsInteger :: YicesTerm -> YicesTerm
realIsInteger YicesTerm
x = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"is-int" [YicesTerm
x]
realDiv :: YicesTerm -> YicesTerm -> YicesTerm
realDiv YicesTerm
x YicesTerm
y = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"/" [YicesTerm
x, YicesTerm
y]
realSin :: YicesTerm -> YicesTerm
realSin = forall a. a
errorComputableUnsupported
realCos :: YicesTerm -> YicesTerm
realCos = forall a. a
errorComputableUnsupported
realTan :: YicesTerm -> YicesTerm
realTan = forall a. a
errorComputableUnsupported
realATan2 :: YicesTerm -> YicesTerm -> YicesTerm
realATan2 = forall a. a
errorComputableUnsupported
realSinh :: YicesTerm -> YicesTerm
realSinh = forall a. a
errorComputableUnsupported
realCosh :: YicesTerm -> YicesTerm
realCosh = forall a. a
errorComputableUnsupported
realTanh :: YicesTerm -> YicesTerm
realTanh = forall a. a
errorComputableUnsupported
realExp :: YicesTerm -> YicesTerm
realExp = forall a. a
errorComputableUnsupported
realLog :: YicesTerm -> YicesTerm
realLog = forall a. a
errorComputableUnsupported
smtFnApp :: YicesTerm -> [YicesTerm] -> YicesTerm
smtFnApp YicesTerm
nm [YicesTerm]
args = Builder -> [YicesTerm] -> YicesTerm
term_app (YicesTerm -> Builder
renderTerm YicesTerm
nm) [YicesTerm]
args
smtFnUpdate :: Maybe (YicesTerm -> [YicesTerm] -> YicesTerm -> YicesTerm)
smtFnUpdate = forall a. Maybe a
Nothing
lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> YicesTerm -> YicesTerm)
lambdaTerm = forall a. a -> Maybe a
Just [(Text, Some TypeMap)] -> YicesTerm -> YicesTerm
yicesLambda
floatTerm :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BigFloat -> YicesTerm
floatTerm FloatPrecisionRepr fpp
_ BigFloat
_ = forall a. (?callStack::CallStack) => a
floatFail
floatNeg :: YicesTerm -> YicesTerm
floatNeg YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatAbs :: YicesTerm -> YicesTerm
floatAbs YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatSqrt :: RoundingMode -> YicesTerm -> YicesTerm
floatSqrt RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatAdd :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm
floatAdd RoundingMode
_ YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatSub :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm
floatSub RoundingMode
_ YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatMul :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm
floatMul RoundingMode
_ YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatDiv :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm
floatDiv RoundingMode
_ YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatRem :: YicesTerm -> YicesTerm -> YicesTerm
floatRem YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatFMA :: RoundingMode -> YicesTerm -> YicesTerm -> YicesTerm -> YicesTerm
floatFMA RoundingMode
_ YicesTerm
_ YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatEq :: YicesTerm -> YicesTerm -> YicesTerm
floatEq YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatFpEq :: YicesTerm -> YicesTerm -> YicesTerm
floatFpEq YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatLe :: YicesTerm -> YicesTerm -> YicesTerm
floatLe YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatLt :: YicesTerm -> YicesTerm -> YicesTerm
floatLt YicesTerm
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatIsNaN :: YicesTerm -> YicesTerm
floatIsNaN YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatIsInf :: YicesTerm -> YicesTerm
floatIsInf YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatIsZero :: YicesTerm -> YicesTerm
floatIsZero YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatIsPos :: YicesTerm -> YicesTerm
floatIsPos YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatIsNeg :: YicesTerm -> YicesTerm
floatIsNeg YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatIsSubnorm :: YicesTerm -> YicesTerm
floatIsSubnorm YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatIsNorm :: YicesTerm -> YicesTerm
floatIsNorm YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatCast :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
floatCast FloatPrecisionRepr fpp
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatRound :: RoundingMode -> YicesTerm -> YicesTerm
floatRound RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatFromBinary :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> YicesTerm -> YicesTerm
floatFromBinary FloatPrecisionRepr fpp
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
bvToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
bvToFloat FloatPrecisionRepr fpp
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
sbvToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
sbvToFloat FloatPrecisionRepr fpp
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
realToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> YicesTerm -> YicesTerm
realToFloat FloatPrecisionRepr fpp
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatToBV :: Nat -> RoundingMode -> YicesTerm -> YicesTerm
floatToBV Nat
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatToSBV :: Nat -> RoundingMode -> YicesTerm -> YicesTerm
floatToSBV Nat
_ RoundingMode
_ YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
floatToReal :: YicesTerm -> YicesTerm
floatToReal YicesTerm
_ = forall a. (?callStack::CallStack) => a
floatFail
fromText :: Text -> YicesTerm
fromText Text
t = Builder -> YicesTerm
T (Text -> Builder
Builder.fromText Text
t)
unsupportedFeature :: String -> a
unsupportedFeature :: forall a. [Char] -> a
unsupportedFeature [Char]
s = forall a. (?callStack::CallStack) => [Char] -> a
error ([Char]
"Yices does not support " forall a. Semigroup a => a -> a -> a
<> [Char]
s)
floatFail :: HasCallStack => a
floatFail :: forall a. (?callStack::CallStack) => a
floatFail = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"Yices does not support IEEE-754 floating-point numbers"
stringFail :: HasCallStack => a
stringFail :: forall a. (?callStack::CallStack) => a
stringFail = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"Yices does not support strings"
errorComputableUnsupported :: a
errorComputableUnsupported :: forall a. a
errorComputableUnsupported = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"computable functions are not supported."
newtype YicesType = YicesType { YicesType -> Builder
unType :: Builder }
tupleType :: [YicesType] -> YicesType
tupleType :: [YicesType] -> YicesType
tupleType [] = Builder -> YicesType
YicesType Builder
"unit-type"
tupleType [YicesType]
flds = Builder -> YicesType
YicesType (Builder -> [Builder] -> Builder
app Builder
"tuple" (YicesType -> Builder
unType forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [YicesType]
flds))
boolType :: YicesType
boolType :: YicesType
boolType = Builder -> YicesType
YicesType Builder
"bool"
intType :: YicesType
intType :: YicesType
intType = Builder -> YicesType
YicesType Builder
"int"
realType :: YicesType
realType :: YicesType
realType = Builder -> YicesType
YicesType Builder
"real"
fnType :: [YicesType] -> YicesType -> YicesType
fnType :: [YicesType] -> YicesType -> YicesType
fnType [] YicesType
tp = YicesType
tp
fnType [YicesType]
args YicesType
tp = Builder -> YicesType
YicesType forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"->" (YicesType -> Builder
unType forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ([YicesType]
args forall a. [a] -> [a] -> [a]
++ [YicesType
tp]))
yicesType :: TypeMap tp -> YicesType
yicesType :: forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType TypeMap tp
BoolTypeMap = YicesType
boolType
yicesType TypeMap tp
IntegerTypeMap = YicesType
intType
yicesType TypeMap tp
RealTypeMap = YicesType
realType
yicesType (BVTypeMap NatRepr w
w) = Builder -> YicesType
YicesType (Builder -> [Builder] -> Builder
app Builder
"bitvector" [forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show NatRepr w
w)])
yicesType (FloatTypeMap FloatPrecisionRepr fpp
_) = forall a. (?callStack::CallStack) => a
floatFail
yicesType TypeMap tp
UnicodeTypeMap = forall a. (?callStack::CallStack) => a
stringFail
yicesType TypeMap tp
ComplexToStructTypeMap = [YicesType] -> YicesType
tupleType [YicesType
realType, YicesType
realType]
yicesType TypeMap tp
ComplexToArrayTypeMap = [YicesType] -> YicesType -> YicesType
fnType [YicesType
boolType] YicesType
realType
yicesType (PrimArrayTypeMap Assignment TypeMap (idxl ::> idx)
i TypeMap tp1
r) = [YicesType] -> YicesType -> YicesType
fnType (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap (idxl ::> idx)
i) (forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType TypeMap tp1
r)
yicesType (FnArrayTypeMap Assignment TypeMap (idxl ::> idx)
i TypeMap tp1
r) = [YicesType] -> YicesType -> YicesType
fnType (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap (idxl ::> idx)
i) (forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType TypeMap tp1
r)
yicesType (StructTypeMap Assignment TypeMap idx
f) = [YicesType] -> YicesType
tupleType (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap idx
f)
assertForallCommand :: [(Text,YicesType)] -> Expr -> Command Connection
assertForallCommand :: [(Text, YicesType)] -> YicesTerm -> Command Connection
assertForallCommand [(Text, YicesType)]
vars YicesTerm
e = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert" [YicesTerm -> Builder
renderTerm YicesTerm
res]
where res :: YicesTerm
res = Builder -> [Builder] -> YicesTerm -> YicesTerm
binder_app Builder
"forall" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> YicesType -> Builder
mkBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, YicesType)]
vars) YicesTerm
e
mkBinding :: Text -> YicesType -> Builder
mkBinding Text
nm YicesType
tp = Text -> Builder
Builder.fromText Text
nm forall a. Semigroup a => a -> a -> a
<> Builder
"::" forall a. Semigroup a => a -> a -> a
<> YicesType -> Builder
unType YicesType
tp
efSolveCommand :: Command Connection
efSolveCommand :: Command Connection
efSolveCommand Connection
_ = Builder -> YicesCommand
safeCmd Builder
"(ef-solve)"
evalCommand :: Term Connection -> Command Connection
evalCommand :: Term Connection -> Command Connection
evalCommand Term Connection
v Connection
_ = Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"eval" [YicesTerm -> Builder
renderTerm Term Connection
v]
exitCommand :: Command Connection
exitCommand :: Command Connection
exitCommand Connection
_ = Builder -> YicesCommand
safeCmd Builder
"(exit)"
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)"
setParamCommand :: Text -> Builder -> Command Connection
setParamCommand :: Text -> Builder -> Command Connection
setParamCommand Text
nm Builder
v Connection
_ = Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"set-param" [ Text -> Builder
Builder.fromText Text
nm, Builder
v ]
setTimeoutCommand :: Command Connection
setTimeoutCommand :: Command Connection
setTimeoutCommand Connection
conn = Builder -> YicesCommand
unsafeCmd forall a b. (a -> b) -> a -> b
$
Builder -> [Builder] -> Builder
app Builder
"set-timeout" [ [Char] -> Builder
Builder.fromString (forall a. Show a => a -> [Char]
show (SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds forall a b. (a -> b) -> a -> b
$ Connection -> SolverGoalTimeout
yicesTimeout Connection
conn)) ]
declareUnitTypeCommand :: Command Connection
declareUnitTypeCommand :: Command Connection
declareUnitTypeCommand Connection
_conn = Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$
Builder -> [Builder] -> Builder
app Builder
"define-type" [ [Char] -> Builder
Builder.fromString [Char]
"unit-type", Builder -> [Builder] -> Builder
app Builder
"scalar" [ [Char] -> Builder
Builder.fromString [Char]
"unit-value" ] ]
declareUnitType :: WriterConn t Connection -> IO ()
declareUnitType :: forall t. WriterConn t Connection -> IO ()
declareUnitType WriterConn t Connection
conn =
do Bool
done <- forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef (Connection -> IORef Bool
yicesUnitDeclared (forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn)) (\Bool
x -> (Bool
True, Bool
x))
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless Bool
done forall a b. (a -> b) -> a -> b
$ forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t Connection
conn Command Connection
declareUnitTypeCommand
resetUnitType :: WriterConn t Connection -> IO ()
resetUnitType :: forall t. WriterConn t Connection -> IO ()
resetUnitType WriterConn t Connection
conn =
forall a. IORef a -> a -> IO ()
writeIORef (Connection -> IORef Bool
yicesUnitDeclared (forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn)) Bool
False
newConnection ::
Streams.OutputStream Text ->
Streams.InputStream Text ->
(IORef (Maybe Int) -> AcknowledgementAction t Connection) ->
ProblemFeatures ->
SolverGoalTimeout ->
B.SymbolVarBimap t ->
IO (WriterConn t Connection)
newConnection :: forall t.
OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
newConnection OutputStream Text
stream InputStream Text
in_stream IORef (Maybe Int) -> AcknowledgementAction t Connection
ack ProblemFeatures
reqFeatures SolverGoalTimeout
timeout SymbolVarBimap t
bindings = do
let efSolver :: Bool
efSolver = ProblemFeatures
reqFeatures ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useExistForall
let nlSolver :: Bool
nlSolver = ProblemFeatures
reqFeatures ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useNonlinearArithmetic
let features :: ProblemFeatures
features | Bool
efSolver = ProblemFeatures
useLinearArithmetic
| Bool
nlSolver = ProblemFeatures
useNonlinearArithmetic forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
| Bool
otherwise = ProblemFeatures
reqFeatures
let nm :: [Char]
nm | Bool
efSolver = [Char]
"Yices ef-solver"
| Bool
nlSolver = [Char]
"Yices nl-solver"
| Bool
otherwise = [Char]
"Yices"
let featureIf :: Bool -> ProblemFeatures -> ProblemFeatures
featureIf Bool
True ProblemFeatures
f = ProblemFeatures
f
featureIf Bool
False ProblemFeatures
_ = ProblemFeatures
noFeatures
let features' :: ProblemFeatures
features' = ProblemFeatures
features
forall a. Bits a => a -> a -> a
.|. Bool -> ProblemFeatures -> ProblemFeatures
featureIf Bool
efSolver ProblemFeatures
useExistForall
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStructs
forall a. Bits a => a -> a -> a
.|. (ProblemFeatures
reqFeatures forall a. Bits a => a -> a -> a
.&. (ProblemFeatures
useUnsatCores forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useUnsatAssumptions))
IORef (Maybe Int)
earlyUnsatRef <- forall a. a -> IO (IORef a)
newIORef forall a. Maybe a
Nothing
IORef Bool
unitRef <- forall a. a -> IO (IORef a)
newIORef Bool
False
let c :: Connection
c = Connection { yicesEarlyUnsat :: IORef (Maybe Int)
yicesEarlyUnsat = IORef (Maybe Int)
earlyUnsatRef
, yicesTimeout :: SolverGoalTimeout
yicesTimeout = SolverGoalTimeout
timeout
, yicesUnitDeclared :: IORef Bool
yicesUnitDeclared = IORef Bool
unitRef
}
WriterConn t Connection
conn <- forall t cs.
OutputStream Text
-> InputStream Text
-> AcknowledgementAction t cs
-> [Char]
-> ResponseStrictness
-> ProblemFeatures
-> SymbolVarBimap t
-> cs
-> IO (WriterConn t cs)
newWriterConn OutputStream Text
stream InputStream Text
in_stream (IORef (Maybe Int) -> AcknowledgementAction t Connection
ack IORef (Maybe Int)
earlyUnsatRef) [Char]
nm ResponseStrictness
Strict ProblemFeatures
features' SymbolVarBimap t
bindings Connection
c
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! WriterConn t Connection
conn { supportFunctionDefs :: Bool
supportFunctionDefs = Bool
True
, supportFunctionArguments :: Bool
supportFunctionArguments = Bool
True
, supportQuantifiers :: Bool
supportQuantifiers = Bool
efSolver
}
data YicesCommand = YicesCommand
{ YicesCommand -> Bool
cmdEarlyUnsatSafe :: Bool
, YicesCommand -> Builder
cmdCmd :: Builder
}
safeCmd :: Builder -> YicesCommand
safeCmd :: Builder -> YicesCommand
safeCmd Builder
txt = YicesCommand { cmdEarlyUnsatSafe :: Bool
cmdEarlyUnsatSafe = Bool
True, cmdCmd :: Builder
cmdCmd = Builder
txt }
unsafeCmd :: Builder -> YicesCommand
unsafeCmd :: Builder -> YicesCommand
unsafeCmd Builder
txt = YicesCommand { cmdEarlyUnsatSafe :: Bool
cmdEarlyUnsatSafe = Bool
False, cmdCmd :: Builder
cmdCmd = Builder
txt }
type instance Term Connection = YicesTerm
type instance Command Connection = Connection -> YicesCommand
instance SMTWriter Connection where
forallExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection
forallExpr [(Text, Some TypeMap)]
vars Term Connection
t = Builder -> [Builder] -> YicesTerm -> YicesTerm
binder_app Builder
"forall" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Some TypeMap -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
vars) Term Connection
t
existsExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection
existsExpr [(Text, Some TypeMap)]
vars Term Connection
t = Builder -> [Builder] -> YicesTerm -> YicesTerm
binder_app Builder
"exists" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Some TypeMap -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
vars) Term Connection
t
arraySelect :: Term Connection -> [Term Connection] -> Term Connection
arraySelect = forall v. SupportTermOps v => v -> [v] -> v
smtFnApp
arrayUpdate :: Term Connection
-> [Term Connection] -> Term Connection -> Term Connection
arrayUpdate Term Connection
a [Term Connection]
i Term Connection
v =
Builder -> YicesTerm
T forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"update" [ YicesTerm -> Builder
renderTerm Term Connection
a, [Builder] -> Builder
builder_list (YicesTerm -> Builder
renderTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term Connection]
i), YicesTerm -> Builder
renderTerm Term Connection
v ]
commentCommand :: forall (f :: Type -> Type).
f Connection -> Builder -> Command Connection
commentCommand f Connection
_ Builder
b = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd (Builder
";; " forall a. Semigroup a => a -> a -> a
<> Builder
b)
pushCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
pushCommand f Connection
_ = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(push)"
popCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
popCommand f Connection
_ = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(pop)"
push2Command :: forall (f :: Type -> Type). f Connection -> Command Connection
push2Command f Connection
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"(push 2)"
pop2Command :: forall (f :: Type -> Type). f Connection -> Command Connection
pop2Command f Connection
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"(pop 2)"
resetCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
resetCommand f Connection
_ = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(reset)"
checkCommands :: forall (f :: Type -> Type). f Connection -> [Command Connection]
checkCommands f Connection
_ =
[ Command Connection
setTimeoutCommand, forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(check)" ]
checkWithAssumptionsCommands :: forall (f :: Type -> Type).
f Connection -> [Text] -> [Command Connection]
checkWithAssumptionsCommands f Connection
_ [Text]
nms =
[ Command Connection
setTimeoutCommand
, forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app_list Builder
"check-assuming" (forall a b. (a -> b) -> [a] -> [b]
map Text -> Builder
Builder.fromText [Text]
nms)
]
getUnsatAssumptionsCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
getUnsatAssumptionsCommand f Connection
_ = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(show-unsat-assumptions)"
getUnsatCoreCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
getUnsatCoreCommand f Connection
_ = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd Builder
"(show-unsat-core)"
getAbductCommand :: forall (f :: Type -> Type).
f Connection -> Text -> Term Connection -> Command Connection
getAbductCommand f Connection
_ Text
_ Term Connection
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"abduction"
getAbductNextCommand :: forall (f :: Type -> Type). f Connection -> Command Connection
getAbductNextCommand f Connection
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"abduction"
setOptCommand :: forall (f :: Type -> Type).
f Connection -> Text -> Text -> Command Connection
setOptCommand f Connection
_ Text
x Text
o = Text -> Builder -> Command Connection
setParamCommand Text
x (Text -> Builder
Builder.fromText Text
o)
assertCommand :: forall (f :: Type -> Type).
f Connection -> Term Connection -> Command Connection
assertCommand f Connection
_ (T Builder
nm) = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert" [Builder
nm]
assertNamedCommand :: forall (f :: Type -> Type).
f Connection -> Term Connection -> Text -> Command Connection
assertNamedCommand f Connection
_ (T Builder
tm) Text
nm = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
unsafeCmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert" [Builder
tm, Text -> Builder
Builder.fromText Text
nm]
declareCommand :: forall (f :: Type -> Type) (args :: Ctx BaseType)
(rtp :: BaseType).
f Connection
-> Text
-> Assignment TypeMap args
-> TypeMap rtp
-> Command Connection
declareCommand f Connection
_ Text
v Assignment TypeMap args
args TypeMap rtp
rtp =
forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$
Builder -> [Builder] -> Builder
app Builder
"define" [Text -> Builder
Builder.fromText Text
v forall a. Semigroup a => a -> a -> a
<> Builder
"::"
forall a. Semigroup a => a -> a -> a
<> YicesType -> Builder
unType ([YicesType] -> YicesType -> YicesType
fnType (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Assignment TypeMap args
args) (forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType TypeMap rtp
rtp))
]
defineCommand :: forall (f :: Type -> Type) (rtp :: BaseType).
f Connection
-> Text
-> [(Text, Some TypeMap)]
-> TypeMap rtp
-> Term Connection
-> Command Connection
defineCommand f Connection
_ Text
v [(Text, Some TypeMap)]
args TypeMap rtp
rtp Term Connection
t =
forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Builder -> YicesCommand
safeCmd forall a b. (a -> b) -> a -> b
$
Builder -> [Builder] -> Builder
app Builder
"define" [Text -> Builder
Builder.fromText Text
v forall a. Semigroup a => a -> a -> a
<> Builder
"::"
forall a. Semigroup a => a -> a -> a
<> YicesType -> Builder
unType ([YicesType] -> YicesType -> YicesType
fnType ((\(Text
_,Some TypeMap
tp) -> forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType Some TypeMap
tp) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
args) (forall (tp :: BaseType). TypeMap tp -> YicesType
yicesType TypeMap rtp
rtp))
, YicesTerm -> Builder
renderTerm ([(Text, Some TypeMap)] -> YicesTerm -> YicesTerm
yicesLambda [(Text, Some TypeMap)]
args Term Connection
t)
]
synthFunCommand :: forall (f :: Type -> Type) (tp :: BaseType).
f Connection
-> Text
-> [(Text, Some TypeMap)]
-> TypeMap tp
-> Command Connection
synthFunCommand f Connection
_ Text
_ [(Text, Some TypeMap)]
_ TypeMap tp
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"SyGuS"
declareVarCommand :: forall (f :: Type -> Type) (tp :: BaseType).
f Connection -> Text -> TypeMap tp -> Command Connection
declareVarCommand f Connection
_ Text
_ TypeMap tp
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"SyGuS"
constraintCommand :: forall (f :: Type -> Type).
f Connection -> Term Connection -> Command Connection
constraintCommand f Connection
_ Term Connection
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"SyGuS"
resetDeclaredStructs :: forall t. WriterConn t Connection -> IO ()
resetDeclaredStructs WriterConn t Connection
conn = forall t. WriterConn t Connection -> IO ()
resetUnitType WriterConn t Connection
conn
structProj :: forall (args :: Ctx BaseType) (tp :: BaseType).
Assignment TypeMap args
-> Index args tp -> Term Connection -> Term Connection
structProj Assignment TypeMap args
_n Index args tp
i Term Connection
s = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"select" [Term Connection
s, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index args tp
i forall a. Num a => a -> a -> a
+ Int
1)]
structCtor :: forall (args :: Ctx BaseType).
Assignment TypeMap args -> [Term Connection] -> Term Connection
structCtor Assignment TypeMap args
_tps [] = Builder -> YicesTerm
T Builder
"unit-value"
structCtor Assignment TypeMap args
_tps [Term Connection]
args = Builder -> [YicesTerm] -> YicesTerm
term_app Builder
"mk-tuple" [Term Connection]
args
stringTerm :: Text -> Term Connection
stringTerm Text
_ = forall a. (?callStack::CallStack) => a
stringFail
stringLength :: Term Connection -> Term Connection
stringLength Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
stringAppend :: [Term Connection] -> Term Connection
stringAppend [Term Connection]
_ = forall a. (?callStack::CallStack) => a
stringFail
stringContains :: Term Connection -> Term Connection -> Term Connection
stringContains Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
stringIndexOf :: Term Connection
-> Term Connection -> Term Connection -> Term Connection
stringIndexOf Term Connection
_ Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection
stringIsPrefixOf Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection
stringIsSuffixOf Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
stringSubstring :: Term Connection
-> Term Connection -> Term Connection -> Term Connection
stringSubstring Term Connection
_ Term Connection
_ Term Connection
_ = forall a. (?callStack::CallStack) => a
stringFail
declareStructDatatype :: forall t (args :: Ctx BaseType).
WriterConn t Connection -> Assignment TypeMap args -> IO ()
declareStructDatatype WriterConn t Connection
conn Assignment TypeMap args
Ctx.Empty = forall t. WriterConn t Connection -> IO ()
declareUnitType WriterConn t Connection
conn
declareStructDatatype WriterConn t Connection
_ Assignment TypeMap args
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
writeCommand :: forall t. WriterConn t Connection -> Command Connection -> IO ()
writeCommand WriterConn t Connection
conn Command Connection
cmdf =
do Maybe Int
isEarlyUnsat <- forall a. IORef a -> IO a
readIORef (Connection -> IORef (Maybe Int)
yicesEarlyUnsat (forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn))
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (forall a. Maybe a -> Bool
isJust Maybe Int
isEarlyUnsat Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
earlyUnsatSafe) forall a b. (a -> b) -> a -> b
$ do
forall a. Maybe a -> OutputStream a -> IO ()
Streams.write (forall a. a -> Maybe a
Just Text
cmdout) (forall t h. WriterConn t h -> OutputStream Text
connHandle WriterConn t Connection
conn)
forall a. Maybe a -> OutputStream a -> IO ()
Streams.write (forall a. a -> Maybe a
Just Text
"") (forall t h. WriterConn t h -> OutputStream Text
connHandle WriterConn t Connection
conn)
where
cmd :: YicesCommand
cmd = Command Connection
cmdf (forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn)
earlyUnsatSafe :: Bool
earlyUnsatSafe = YicesCommand -> Bool
cmdEarlyUnsatSafe YicesCommand
cmd
cmdBuilder :: Builder
cmdBuilder = YicesCommand -> Builder
cmdCmd YicesCommand
cmd
cmdout :: Text
cmdout = Text -> Text
Lazy.toStrict (Builder -> Text
Builder.toLazyText Builder
cmdBuilder) forall a. Semigroup a => a -> a -> a
<> Text
"\n"
instance SMTReadWriter Connection where
smtEvalFuns :: forall t.
WriterConn t Connection
-> InputStream Text -> SMTEvalFunctions Connection
smtEvalFuns WriterConn t Connection
conn InputStream Text
resp =
SMTEvalFunctions { smtEvalBool :: Term Connection -> IO Bool
smtEvalBool = forall s. Eval s Bool
yicesEvalBool WriterConn t Connection
conn InputStream Text
resp
, smtEvalBV :: forall (w :: Nat). NatRepr w -> Term Connection -> IO (BV w)
smtEvalBV = \NatRepr w
w -> forall (w :: Nat) s. NatRepr w -> Eval s (BV w)
yicesEvalBV NatRepr w
w WriterConn t Connection
conn InputStream Text
resp
, smtEvalReal :: Term Connection -> IO Rational
smtEvalReal = forall s. Eval s Rational
yicesEvalReal WriterConn t Connection
conn InputStream Text
resp
, smtEvalFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> Term Connection -> IO (BV (FloatPrecisionBits fpp))
smtEvalFloat = \FloatPrecisionRepr fpp
_ Term Connection
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Yices does not support floats."
, smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper Connection)
smtEvalBvArray = forall a. Maybe a
Nothing
, smtEvalString :: Term Connection -> IO Text
smtEvalString = \Term Connection
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Yices does not support strings."
}
smtSatResult :: forall (f :: Type -> Type) t.
f Connection -> WriterConn t Connection -> IO (SatResult () ())
smtSatResult f Connection
_ = forall t. WriterConn t Connection -> IO (SatResult () ())
getSatResponse
smtUnsatAssumptionsResult :: forall (f :: Type -> Type) t.
f Connection -> WriterConn t Connection -> IO [(Bool, Text)]
smtUnsatAssumptionsResult f Connection
_ WriterConn t Connection
s =
do Either SomeException SExp
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t Connection
s))
let cmd :: YicesCommand
cmd = Builder -> YicesCommand
safeCmd Builder
"(show-unsat-assumptions)"
case Either SomeException SExp
mb of
Right (SExp -> Maybe [(Bool, Text)]
asNegAtomList -> Just [(Bool, Text)]
as) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return [(Bool, Text)]
as
Right (SApp [SAtom Text
"error", SString Text
msg]) -> forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesError YicesCommand
cmd Text
msg)
Right SExp
res -> forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd ([Char] -> Text
Text.pack (forall a. Show a => a -> [Char]
show SExp
res)))
Left (SomeException e
e) -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd forall a b. (a -> b) -> a -> b
$ [Char] -> Text
Text.pack forall a b. (a -> b) -> a -> b
$
[[Char]] -> [Char]
unlines [ [Char]
"Could not parse unsat assumptions result."
, [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException e
e
]
smtUnsatCoreResult :: forall (f :: Type -> Type) t.
f Connection -> WriterConn t Connection -> IO [Text]
smtUnsatCoreResult f Connection
_ WriterConn t Connection
s =
do Either SomeException SExp
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t Connection
s))
let cmd :: YicesCommand
cmd = Builder -> YicesCommand
safeCmd Builder
"(show-unsat-core)"
case Either SomeException SExp
mb of
Right (SExp -> Maybe [Text]
asAtomList -> Just [Text]
nms) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return [Text]
nms
Right (SApp [SAtom Text
"error", SString Text
msg]) -> forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesError YicesCommand
cmd Text
msg)
Right SExp
res -> forall a e. Exception e => e -> a
throw (YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd ([Char] -> Text
Text.pack (forall a. Show a => a -> [Char]
show SExp
res)))
Left (SomeException e
e) -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ YicesCommand -> Text -> YicesException
YicesParseError YicesCommand
cmd forall a b. (a -> b) -> a -> b
$ [Char] -> Text
Text.pack forall a b. (a -> b) -> a -> b
$
[[Char]] -> [Char]
unlines [ [Char]
"Could not parse unsat core result."
, [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException e
e
]
smtAbductResult :: forall (f :: Type -> Type) t.
f Connection
-> WriterConn t Connection -> Text -> Term Connection -> IO [Char]
smtAbductResult f Connection
_ WriterConn t Connection
_ Text
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"abduction"
smtAbductNextResult :: forall (f :: Type -> Type) t.
f Connection -> WriterConn t Connection -> IO [Char]
smtAbductNextResult f Connection
_ = forall a. [Char] -> a
unsupportedFeature [Char]
"abduction"
data YicesException
= YicesUnsupported YicesCommand
| YicesError YicesCommand Text
| YicesParseError YicesCommand Text
instance Show YicesException where
show :: YicesException -> [Char]
show (YicesUnsupported (YicesCommand Bool
_ Builder
cmd)) =
[[Char]] -> [Char]
unlines
[ [Char]
"unsupported command:"
, [Char]
" " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)
]
show (YicesError (YicesCommand Bool
_ Builder
cmd) Text
msg) =
[[Char]] -> [Char]
unlines
[ [Char]
"Solver reported an error:"
, [Char]
" " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack Text
msg
, [Char]
"in response to command:"
, [Char]
" " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)
]
show (YicesParseError (YicesCommand Bool
_ Builder
cmd) Text
msg) =
[[Char]] -> [Char]
unlines
[ [Char]
"Could not parse solver response:"
, [Char]
" " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack Text
msg
, [Char]
"in response to command:"
, [Char]
" " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)
]
instance Exception YicesException
instance OnlineSolver Connection where
startSolverProcess :: forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope Connection)
startSolverProcess = forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope Connection)
yicesStartSolver
shutdownSolverProcess :: forall scope. SolverProcess scope Connection -> IO (ExitCode, Text)
shutdownSolverProcess = forall scope. SolverProcess scope Connection -> IO (ExitCode, Text)
yicesShutdownSolver
yicesShutdownSolver :: SolverProcess s Connection -> IO (ExitCode, Lazy.Text)
yicesShutdownSolver :: forall scope. SolverProcess scope Connection -> IO (ExitCode, Text)
yicesShutdownSolver SolverProcess s Connection
p =
do forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck (forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess s Connection
p) Command Connection
exitCommand
forall a. Maybe a -> OutputStream a -> IO ()
Streams.write forall a. Maybe a
Nothing (forall t solver. SolverProcess t solver -> OutputStream Text
solverStdin SolverProcess s Connection
p)
Text
txt <- HandleReader -> IO Text
readAllLines (forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess s Connection
p)
HandleReader -> IO ()
stopHandleReader (forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess s Connection
p)
ExitCode
ec <- forall scope solver. SolverProcess scope solver -> IO ExitCode
solverCleanupCallback SolverProcess s Connection
p
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExitCode
ec,Text
txt)
yicesAck ::
IORef (Maybe Int) ->
AcknowledgementAction s Connection
yicesAck :: forall s. IORef (Maybe Int) -> AcknowledgementAction s Connection
yicesAck IORef (Maybe Int)
earlyUnsatRef = forall t h.
(WriterConn t h -> Command h -> IO ()) -> AcknowledgementAction t h
AckAction forall a b. (a -> b) -> a -> b
$ \WriterConn s Connection
conn Command Connection
cmdf ->
do Maybe Int
isEarlyUnsat <- forall a. IORef a -> IO a
readIORef IORef (Maybe Int)
earlyUnsatRef
let cmd :: YicesCommand
cmd = Command Connection
cmdf (forall t h. WriterConn t h -> h
connState WriterConn s Connection
conn)
earlyUnsatSafe :: Bool
earlyUnsatSafe = YicesCommand -> Bool
cmdEarlyUnsatSafe YicesCommand
cmd
cmdBuilder :: Builder
cmdBuilder = YicesCommand -> Builder
cmdCmd YicesCommand
cmd
if forall a. Maybe a -> Bool
isJust Maybe Int
isEarlyUnsat Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
earlyUnsatSafe
then forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
else do
Maybe Text
x <- InputStream Text -> IO (Maybe Text)
getAckResponse (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn s Connection
conn)
case Maybe Text
x of
Maybe Text
Nothing ->
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
Just Text
"unsat" ->
do Int
i <- forall t h. WriterConn t h -> IO Int
entryStackHeight WriterConn s Connection
conn
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe Int)
earlyUnsatRef forall a b. (a -> b) -> a -> b
$! (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! if Int
i forall a. Ord a => a -> a -> Bool
> Int
0 then Int
1 else Int
0)
Just Text
txt ->
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"Unexpected response from solver while awaiting acknowledgement"
, [Char]
"*** result:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Text
txt
, [Char]
"in response to command"
, [Char]
"***: " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmdBuilder)
]
yicesStartSolver ::
ProblemFeatures ->
Maybe Handle ->
B.ExprBuilder t st fs ->
IO (SolverProcess t Connection)
yicesStartSolver :: forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope Connection)
yicesStartSolver ProblemFeatures
features Maybe Handle
auxOutput ExprBuilder t st fs
sym = do
let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
[Char]
yices_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
findSolverPath ConfigOption (BaseStringType Unicode)
yicesPath Config
cfg
Bool
enableMCSat <- forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableMCSat Config
cfg
Bool
enableInteractive <- forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableInteractive Config
cfg
SolverGoalTimeout
goalTimeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
1000forall a. Num a => a -> a -> a
*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
yicesGoalTimeout Config
cfg)
let modeFlag :: [Char]
modeFlag | Bool
enableInteractive
Bool -> Bool -> Bool
|| (SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds SolverGoalTimeout
goalTimeout) forall a. Eq a => a -> a -> Bool
/= Integer
0 = [Char]
"--mode=interactive"
| Bool
otherwise = [Char]
"--mode=push-pop"
args :: [[Char]]
args = [Char]
modeFlag forall a. a -> [a] -> [a]
: [Char]
"--print-success" forall a. a -> [a] -> [a]
:
if Bool
enableMCSat then [[Char]
"--mcsat"] else []
hasNamedAssumptions :: Bool
hasNamedAssumptions = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores Bool -> Bool -> Bool
||
ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatAssumptions
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
enableMCSat Bool -> Bool -> Bool
&& Bool
hasNamedAssumptions) forall a b. (a -> b) -> a -> b
$
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Unsat cores and named assumptions are incompatible with MC-SAT in Yices."
let features' :: ProblemFeatures
features' | Bool
enableMCSat = ProblemFeatures
features forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useNonlinearArithmetic
| Bool
otherwise = ProblemFeatures
features
hdls :: (Handle, Handle, Handle, ProcessHandle)
hdls@(Handle
in_h,Handle
out_h,Handle
err_h,ProcessHandle
ph) <- [Char]
-> [[Char]]
-> Maybe [Char]
-> IO (Handle, Handle, Handle, ProcessHandle)
startProcess [Char]
yices_path [[Char]]
args forall a. Maybe a
Nothing
(OutputStream Text
in_stream, InputStream Text
out_stream, HandleReader
err_reader) <-
Handle
-> Handle
-> Handle
-> Maybe (Text, Handle)
-> IO (OutputStream Text, InputStream Text, HandleReader)
demuxProcessHandles Handle
in_h Handle
out_h Handle
err_h
(forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Handle
x -> (Text
"; ", Handle
x)) Maybe Handle
auxOutput)
OutputStream Text
in_stream' <- forall b a. IO b -> OutputStream a -> IO (OutputStream a)
Streams.atEndOfOutput (Handle -> IO ()
hClose Handle
in_h) OutputStream Text
in_stream
WriterConn t Connection
conn <- forall t.
OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
newConnection OutputStream Text
in_stream' InputStream Text
out_stream forall s. IORef (Maybe Int) -> AcknowledgementAction s Connection
yicesAck ProblemFeatures
features' SolverGoalTimeout
goalTimeout forall t. SymbolVarBimap t
B.emptySymbolVarBimap
forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
conn Config
cfg
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! SolverProcess { solverConn :: WriterConn t Connection
solverConn = WriterConn t Connection
conn
, solverCleanupCallback :: IO ExitCode
solverCleanupCallback = (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
cleanupProcess (Handle, Handle, Handle, ProcessHandle)
hdls
, solverStderr :: HandleReader
solverStderr = HandleReader
err_reader
, solverHandle :: ProcessHandle
solverHandle = ProcessHandle
ph
, solverErrorBehavior :: ErrorBehavior
solverErrorBehavior = ErrorBehavior
ContinueOnError
, solverEvalFuns :: SMTEvalFunctions Connection
solverEvalFuns = forall h t.
SMTReadWriter h =>
WriterConn t h -> InputStream Text -> SMTEvalFunctions h
smtEvalFuns WriterConn t Connection
conn InputStream Text
out_stream
, solverLogFn :: SolverEvent -> IO ()
solverLogFn = forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
, solverName :: [Char]
solverName = [Char]
"Yices"
, solverEarlyUnsat :: IORef (Maybe Int)
solverEarlyUnsat = Connection -> IORef (Maybe Int)
yicesEarlyUnsat (forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn)
, solverSupportsResetAssertions :: Bool
solverSupportsResetAssertions = Bool
True
, solverGoalTimeout :: SolverGoalTimeout
solverGoalTimeout = SolverGoalTimeout
goalTimeout
}
sendCheck :: WriterConn t Connection -> IO ()
sendCheck :: forall t. WriterConn t Connection -> IO ()
sendCheck WriterConn t Connection
c = forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn t Connection
c (forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands WriterConn t Connection
c)
sendCheckExistsForall :: WriterConn t Connection -> IO ()
sendCheckExistsForall :: forall t. WriterConn t Connection -> IO ()
sendCheckExistsForall WriterConn t Connection
c = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c Command Connection
checkExistsForallCommand
assertForall :: WriterConn t Connection -> [(Text, YicesType)] -> Expr -> IO ()
assertForall :: forall t.
WriterConn t Connection
-> [(Text, YicesType)] -> YicesTerm -> IO ()
assertForall WriterConn t Connection
c [(Text, YicesType)]
vars YicesTerm
e = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t Connection
c ([(Text, YicesType)] -> YicesTerm -> Command Connection
assertForallCommand [(Text, YicesType)]
vars YicesTerm
e)
setParam :: WriterConn t Connection -> ConfigValue -> IO ()
setParam :: forall t. WriterConn t Connection -> ConfigValue -> IO ()
setParam WriterConn t Connection
c (ConfigValue ConfigOption tp
o ConcreteVal tp
val) =
case forall (tp :: BaseType). ConfigOption tp -> [Text]
configOptionNameParts ConfigOption tp
o of
[Text
yicesName, Text
nm] | Text
yicesName forall a. Eq a => a -> a -> Bool
== Text
"yices" ->
case forall (tp :: BaseType). ConcreteVal tp -> Maybe Builder
asYicesConfigValue ConcreteVal tp
val of
Just Builder
v ->
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t Connection
c (Text -> Builder -> Command Connection
setParamCommand Text
nm Builder
v)
Maybe Builder
Nothing ->
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"Unknown Yices parameter type:", forall a. Show a => a -> [Char]
show Text
nm]
[Text]
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"not a Yices parameter", forall (tp :: BaseType). ConfigOption tp -> [Char]
configOptionName ConfigOption tp
o]
setYicesParams :: WriterConn t Connection -> Config -> IO ()
setYicesParams :: forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
conn Config
cfg = do
[ConfigValue]
params <- Text -> Config -> IO [ConfigValue]
getConfigValues Text
"yices" Config
cfg
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ConfigValue]
params forall a b. (a -> b) -> a -> b
$ forall t. WriterConn t Connection -> ConfigValue -> IO ()
setParam WriterConn t Connection
conn
eval :: WriterConn t Connection -> Term Connection -> IO ()
eval :: forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn t Connection
c Term Connection
e = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c (Term Connection -> Command Connection
evalCommand Term Connection
e)
sendShowModel :: WriterConn t Connection -> IO ()
sendShowModel :: forall t. WriterConn t Connection -> IO ()
sendShowModel WriterConn t Connection
c = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c Command Connection
showModelCommand
getAckResponse :: Streams.InputStream Text -> IO (Maybe Text)
getAckResponse :: InputStream Text -> IO (Maybe Text)
getAckResponse InputStream Text
resps =
do Either SomeException SExp
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString) InputStream Text
resps)
case Either SomeException SExp
mb of
Right (SAtom Text
"ok") -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Right (SAtom Text
txt) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Text
txt)
Right SExp
res -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$
[[Char]] -> [Char]
unlines [ [Char]
"Could not parse acknowledgement result."
, [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SExp
res
]
Left (SomeException e
e) -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$
[[Char]] -> [Char]
unlines [ [Char]
"Could not parse acknowledgement result."
, [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException e
e
]
getSatResponse :: WriterConn t Connection -> IO (SatResult () ())
getSatResponse :: forall t. WriterConn t Connection -> IO (SatResult () ())
getSatResponse WriterConn t Connection
conn =
let interpretSExpr :: SExp -> SatResult () ()
interpretSExpr = \case
(SAtom Text
"unsat") -> forall mdl core. core -> SatResult mdl core
Unsat ()
(SAtom Text
"sat") -> forall mdl core. mdl -> SatResult mdl core
Sat ()
(SAtom Text
"unknown") -> forall mdl core. SatResult mdl core
Unknown
(SAtom Text
"interrupted") -> forall mdl core. SatResult mdl core
Unknown
SExp
res -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ [Char] -> UnparseableYicesResponse
UnparseableYicesResponse forall a b. (a -> b) -> a -> b
$
[[Char]] -> [Char]
unlines [ [Char]
"Could not parse sat result."
, [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SExp
res
]
tmo :: Integer
tmo = SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds forall a b. (a -> b) -> a -> b
$ Connection -> SolverGoalTimeout
yicesTimeout forall a b. (a -> b) -> a -> b
$ forall t h. WriterConn t h -> h
connState WriterConn t Connection
conn
delay :: Integer
delay = Integer
500
msec2usec :: Int -> Int
msec2usec = (Int
1000 forall a. Num a => a -> a -> a
*)
deadman_tmo :: Int
deadman_tmo = Int -> Int
msec2usec forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger (Integer
tmo forall a. Num a => a -> a -> a
+ Integer
delay)
deadmanTimer :: IO ()
deadmanTimer = Int -> IO ()
threadDelay Int
deadman_tmo
action :: InputStream Text -> IO SExp
action = forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseYicesString)
in if Integer
tmo forall a. Eq a => a -> a -> Bool
== Integer
0
then forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (InputStream Text -> IO SExp
action (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t Connection
conn)) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Right SExp
d -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SExp -> SatResult () ()
interpretSExpr SExp
d
Left SomeException
e -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Could not parse sat result."
, [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException SomeException
e
]
else forall a b. IO a -> IO b -> IO (Either a b)
race IO ()
deadmanTimer (forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync forall a b. (a -> b) -> a -> b
$ InputStream Text -> IO SExp
action (forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t Connection
conn)) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Right (Right SExp
x) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SExp -> SatResult () ()
interpretSExpr SExp
x
Left () -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall mdl core. SatResult mdl core
Unknown
Right (Left SomeException
e) -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Could not parse sat result."
, [Char]
"*** Exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException SomeException
e
]
data UnparseableYicesResponse = UnparseableYicesResponse String deriving Int -> UnparseableYicesResponse -> ShowS
[UnparseableYicesResponse] -> ShowS
UnparseableYicesResponse -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [UnparseableYicesResponse] -> ShowS
$cshowList :: [UnparseableYicesResponse] -> ShowS
show :: UnparseableYicesResponse -> [Char]
$cshow :: UnparseableYicesResponse -> [Char]
showsPrec :: Int -> UnparseableYicesResponse -> ShowS
$cshowsPrec :: Int -> UnparseableYicesResponse -> ShowS
Show
instance Exception UnparseableYicesResponse
type Eval scope ty =
WriterConn scope Connection ->
Streams.InputStream Text ->
Term Connection ->
IO ty
yicesEvalReal :: Eval s Rational
yicesEvalReal :: forall s. Eval s Rational
yicesEvalReal WriterConn s Connection
conn InputStream Text
resp Term Connection
tm =
do forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn s Connection
conn Term Connection
tm
Either SomeException (Root Rational)
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser ()
skipSpaceOrNewline forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Text (Root Rational)
Root.parseYicesRoot) InputStream Text
resp)
case Either SomeException (Root Rational)
mb of
Left (SomeException e
ex) ->
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"Could not parse real value returned by yices: "
, forall e. Exception e => e -> [Char]
displayException e
ex
]
Right Root Rational
r -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Root Rational -> Rational
Root.approximate Root Rational
r
parseYicesString :: Atto.Parser Text
parseYicesString :: Parser Text
parseYicesString = Char -> Parser Char
Atto.char Char
'\"' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser Text
go
where
isStringChar :: Char -> Bool
isStringChar Char
'\"' = Bool
False
isStringChar Char
'\\' = Bool
False
isStringChar Char
'\n' = Bool
False
isStringChar Char
_ = Bool
True
octalDigit :: Parser Char
octalDigit = (Char -> Bool) -> Parser Char
Atto.satisfy ([Char] -> Char -> Bool
Atto.inClass [Char]
"01234567")
octalEscape :: Parser Text
octalEscape =
do [Char]
ds <- forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
Atto.choice [ forall (m :: Type -> Type) a. Monad m => Int -> m a -> m [a]
Atto.count Int
i Parser Char
octalDigit | Int
i <- [ Int
3, Int
2, Int
1] ]
case forall a. (Eq a, Num a) => ReadS a
readOct [Char]
ds of
(Int
c,[Char]
""):[(Int, [Char])]
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Char -> Text
Text.singleton (forall a. Enum a => Int -> a
toEnum Int
c))
[(Int, [Char])]
_ -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
escape :: Parser Text
escape = forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
Atto.choice
[ Parser Text
octalEscape
, Char -> Parser Char
Atto.char Char
'n' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return Text
"\n"
, Char -> Parser Char
Atto.char Char
't' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return Text
"\t"
, Char -> Text
Text.singleton forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char
Atto.anyChar
]
go :: Parser Text
go = do Text
xs <- (Char -> Bool) -> Parser Text
Atto.takeWhile Char -> Bool
isStringChar
(Char -> Parser Char
Atto.char Char
'\"' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return Text
xs)
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (do Char
_ <- Char -> Parser Char
Atto.char Char
'\\'
Text
e <- Parser Text
escape
Text
ys <- Parser Text
go
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
xs forall a. Semigroup a => a -> a -> a
<> Text
e forall a. Semigroup a => a -> a -> a
<> Text
ys))
boolValue :: Atto.Parser Bool
boolValue :: Parser Bool
boolValue =
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ Text -> Parser Text
Atto.string Text
"true" forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
, Text -> Parser Text
Atto.string Text
"false" forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
]
yicesEvalBool :: Eval s Bool
yicesEvalBool :: forall s. Eval s Bool
yicesEvalBool WriterConn s Connection
conn InputStream Text
resp Term Connection
tm =
do forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn s Connection
conn Term Connection
tm
Either SomeException Bool
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser ()
skipSpaceOrNewline forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Bool
boolValue) InputStream Text
resp)
case Either SomeException Bool
mb of
Left (SomeException e
ex) ->
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"Could not parse boolean value returned by yices: "
, forall e. Exception e => e -> [Char]
displayException e
ex
]
Right Bool
b -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
b
yicesBV :: Int -> Atto.Parser Integer
yicesBV :: Int -> Parser Integer
yicesBV Int
w =
do Text
_ <- Text -> Parser Text
Atto.string Text
"0b"
Text
digits <- (Char -> Bool) -> Parser Text
Atto.takeWhile (forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` ([Char]
"01"::String))
forall (m :: Type -> Type).
MonadFail m =>
Int -> [Char] -> m Integer
readBit Int
w (Text -> [Char]
Text.unpack Text
digits)
yicesEvalBV :: NatRepr w -> Eval s (BV.BV w)
yicesEvalBV :: forall (w :: Nat) s. NatRepr w -> Eval s (BV w)
yicesEvalBV NatRepr w
w WriterConn s Connection
conn InputStream Text
resp Term Connection
tm =
do forall t. WriterConn t Connection -> Term Connection -> IO ()
eval WriterConn s Connection
conn Term Connection
tm
Either SomeException Integer
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser ()
skipSpaceOrNewline forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Int -> Parser Integer
yicesBV (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w)) InputStream Text
resp)
case Either SomeException Integer
mb of
Left (SomeException e
ex) ->
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"Could not parse bitvector value returned by yices: "
, forall e. Exception e => e -> [Char]
displayException e
ex
]
Right Integer
b -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
b)
readBit :: MonadFail m => Int -> String -> m Integer
readBit :: forall (m :: Type -> Type).
MonadFail m =>
Int -> [Char] -> m Integer
readBit Int
w0 = Int -> Integer -> [Char] -> m Integer
go Int
0 Integer
0
where go :: Int -> Integer -> [Char] -> m Integer
go Int
n Integer
v [Char]
"" = do
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Eq a => a -> a -> Bool
/= Int
w0) forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Value has a different number of bits than we expected."
forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
v
go Int
n Integer
v (Char
c:[Char]
r) = do
case Char
c of
Char
'0' -> Int -> Integer -> [Char] -> m Integer
go (Int
nforall a. Num a => a -> a -> a
+Int
1) (Integer
v forall a. Bits a => a -> Int -> a
`shiftL` Int
1) [Char]
r
Char
'1' -> Int -> Integer -> [Char] -> m Integer
go (Int
nforall a. Num a => a -> a -> a
+Int
1) ((Integer
v forall a. Bits a => a -> Int -> a
`shiftL` Int
1) forall a. Num a => a -> a -> a
+ Integer
1) [Char]
r
Char
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Not a bitvector."
yicesSMT2Features :: ProblemFeatures
yicesSMT2Features :: ProblemFeatures
yicesSMT2Features
= ProblemFeatures
useComputableReals
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
yicesDefaultFeatures :: ProblemFeatures
yicesDefaultFeatures :: ProblemFeatures
yicesDefaultFeatures
= ProblemFeatures
useIntegerArithmetic
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStructs
yicesAdapter :: SolverAdapter t
yicesAdapter :: forall (t :: Type -> Type). SolverAdapter t
yicesAdapter =
SolverAdapter
{ solver_adapter_name :: [Char]
solver_adapter_name = [Char]
"yices"
, solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
yicesOptions
, solver_adapter_check_sat :: forall t fs a.
ExprBuilder t t fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a
solver_adapter_check_sat = \ExprBuilder t t fs
sym LogData
logData [BoolExpr t]
ps SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
cont ->
forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t) () -> IO a)
-> IO a
runYicesInOverride ExprBuilder t t fs
sym LogData
logData [BoolExpr t]
ps
(SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: Type -> Type) a q b r.
Applicative t =>
(a -> t q) -> (b -> t r) -> SatResult a b -> t (SatResult q r)
traverseSatResult (\GroundEvalFn t
x -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (GroundEvalFn t
x,forall a. Maybe a
Nothing)) forall (f :: Type -> Type) a. Applicative f => a -> f a
pure)
, solver_adapter_write_smt2 :: forall t fs. ExprBuilder t t fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 =
forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> [Char]
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
writeDefaultSMT2 () [Char]
"YICES" ProblemFeatures
yicesSMT2Features (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
yicesStrictParsing)
}
yicesPath :: ConfigOption (BaseStringType Unicode)
yicesPath :: ConfigOption (BaseStringType Unicode)
yicesPath = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"solver.yices.path"
yicesPathOLD :: ConfigOption (BaseStringType Unicode)
yicesPathOLD :: ConfigOption (BaseStringType Unicode)
yicesPathOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"yices_path"
yicesEnableMCSat :: ConfigOption BaseBoolType
yicesEnableMCSat :: ConfigOption BaseBoolType
yicesEnableMCSat = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"solver.yices.enable-mcsat"
yicesEnableMCSatOLD :: ConfigOption BaseBoolType
yicesEnableMCSatOLD :: ConfigOption BaseBoolType
yicesEnableMCSatOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"yices_enable-mcsat"
yicesEnableInteractive :: ConfigOption BaseBoolType
yicesEnableInteractive :: ConfigOption BaseBoolType
yicesEnableInteractive = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"solver.yices.enable-interactive"
yicesEnableInteractiveOLD :: ConfigOption BaseBoolType
yicesEnableInteractiveOLD :: ConfigOption BaseBoolType
yicesEnableInteractiveOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"yices_enable-interactive"
yicesGoalTimeout :: ConfigOption BaseIntegerType
yicesGoalTimeout :: ConfigOption BaseIntegerType
yicesGoalTimeout = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"solver.yices.goal-timeout"
yicesGoalTimeoutOLD :: ConfigOption BaseIntegerType
yicesGoalTimeoutOLD :: ConfigOption BaseIntegerType
yicesGoalTimeoutOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"yices_goal-timeout"
yicesStrictParsing :: ConfigOption BaseBoolType
yicesStrictParsing :: ConfigOption BaseBoolType
yicesStrictParsing = forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr [Char]
"solver.yices.strict_parsing"
yicesOptions :: [ConfigDesc]
yicesOptions :: [ConfigDesc]
yicesOptions =
let mkPath :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
co = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption (BaseStringType Unicode)
co
OptionStyle (BaseStringType Unicode)
executablePathOptSty
(forall a. a -> Maybe a
Just Doc Void
"Yices executable path")
(forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString StringLiteral Unicode
"yices"))
mkMCSat :: ConfigOption BaseBoolType -> ConfigDesc
mkMCSat ConfigOption BaseBoolType
co = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseBoolType
co
OptionStyle BaseBoolType
boolOptSty
(forall a. a -> Maybe a
Just Doc Void
"Enable the Yices MCSAT solving engine")
(forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))
mkIntr :: ConfigOption BaseBoolType -> ConfigDesc
mkIntr ConfigOption BaseBoolType
co = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseBoolType
co
OptionStyle BaseBoolType
boolOptSty
(forall a. a -> Maybe a
Just Doc Void
"Enable Yices interactive mode (needed to support timeouts)")
(forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))
mkTmout :: ConfigOption BaseIntegerType -> ConfigDesc
mkTmout ConfigOption BaseIntegerType
co = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
co
OptionStyle BaseIntegerType
integerOptSty
(forall a. a -> Maybe a
Just Doc Void
"Set a per-goal timeout")
(forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
0))
p :: ConfigDesc
p = ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
yicesPath
m :: ConfigDesc
m = ConfigOption BaseBoolType -> ConfigDesc
mkMCSat ConfigOption BaseBoolType
yicesEnableMCSat
i :: ConfigDesc
i = ConfigOption BaseBoolType -> ConfigDesc
mkIntr ConfigOption BaseBoolType
yicesEnableInteractive
t :: ConfigDesc
t = ConfigOption BaseIntegerType -> ConfigDesc
mkTmout ConfigOption BaseIntegerType
yicesGoalTimeout
in [ ConfigDesc
p, ConfigDesc
m, ConfigDesc
i, ConfigDesc
t
, (Text -> Text) -> ConfigDesc -> ConfigDesc
copyOpt (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). ConfigOption tp -> Text
configOptionText ConfigOption BaseBoolType
yicesStrictParsing) ConfigDesc
strictSMTParseOpt
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
p] forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
yicesPathOLD
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
m] forall a b. (a -> b) -> a -> b
$ ConfigOption BaseBoolType -> ConfigDesc
mkMCSat ConfigOption BaseBoolType
yicesEnableMCSatOLD
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
i] forall a b. (a -> b) -> a -> b
$ ConfigOption BaseBoolType -> ConfigDesc
mkIntr ConfigOption BaseBoolType
yicesEnableInteractiveOLD
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
t] forall a b. (a -> b) -> a -> b
$ ConfigOption BaseIntegerType -> ConfigDesc
mkTmout ConfigOption BaseIntegerType
yicesGoalTimeoutOLD
]
forall a. [a] -> [a] -> [a]
++ [ConfigDesc]
yicesInternalOptions
yicesBranchingChoices :: Set Text
yicesBranchingChoices :: Set Text
yicesBranchingChoices = forall a. Ord a => [a] -> Set a
Set.fromList
[ Text
"default"
, Text
"negative"
, Text
"positive"
, Text
"theory"
, Text
"th-pos"
, Text
"th-neg"
]
yicesEFGenModes :: Set Text
yicesEFGenModes :: Set Text
yicesEFGenModes = forall a. Ord a => [a] -> Set a
Set.fromList
[ Text
"auto"
, Text
"none"
, Text
"substitution"
, Text
"projection"
]
booleanOpt :: String -> [ConfigDesc]
booleanOpt :: [Char] -> [ConfigDesc]
booleanOpt [Char]
nm =
let b :: ConfigDesc
b = ConfigOption BaseBoolType -> ConfigDesc
booleanOpt' (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
BaseBoolRepr ([Char]
"solver.yices."forall a. [a] -> [a] -> [a]
++[Char]
nm))
in [ ConfigDesc
b
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
b] forall a b. (a -> b) -> a -> b
$ ConfigOption BaseBoolType -> ConfigDesc
booleanOpt' (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
BaseBoolRepr ([Char]
"yices."forall a. [a] -> [a] -> [a]
++[Char]
nm))
]
booleanOpt' :: ConfigOption BaseBoolType -> ConfigDesc
booleanOpt' :: ConfigOption BaseBoolType -> ConfigDesc
booleanOpt' ConfigOption BaseBoolType
o =
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseBoolType
o
OptionStyle BaseBoolType
boolOptSty
forall a. Maybe a
Nothing
forall a. Maybe a
Nothing
floatWithRangeOpt :: String -> Rational -> Rational -> [ConfigDesc]
floatWithRangeOpt :: [Char] -> Rational -> Rational -> [ConfigDesc]
floatWithRangeOpt [Char]
nm Rational
lo Rational
hi =
let mkO :: [Char] -> ConfigDesc
mkO [Char]
n = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr 'BaseRealType
BaseRealRepr forall a b. (a -> b) -> a -> b
$ [Char]
nforall a. [a] -> [a] -> [a]
++[Char]
nm)
(Bound Rational -> Bound Rational -> OptionStyle 'BaseRealType
realWithRangeOptSty (forall r. r -> Bound r
Inclusive Rational
lo) (forall r. r -> Bound r
Inclusive Rational
hi))
forall a. Maybe a
Nothing
forall a. Maybe a
Nothing
f :: ConfigDesc
f = [Char] -> ConfigDesc
mkO [Char]
"solver.yices."
in [ ConfigDesc
f
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
f] forall a b. (a -> b) -> a -> b
$ [Char] -> ConfigDesc
mkO [Char]
"yices."
]
floatWithMinOpt :: String -> Bound Rational -> [ConfigDesc]
floatWithMinOpt :: [Char] -> Bound Rational -> [ConfigDesc]
floatWithMinOpt [Char]
nm Bound Rational
lo =
let mkO :: [Char] -> ConfigDesc
mkO [Char]
n = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr 'BaseRealType
BaseRealRepr forall a b. (a -> b) -> a -> b
$ [Char]
nforall a. [a] -> [a] -> [a]
++[Char]
nm)
(Bound Rational -> OptionStyle 'BaseRealType
realWithMinOptSty Bound Rational
lo)
forall a. Maybe a
Nothing
forall a. Maybe a
Nothing
f :: ConfigDesc
f = [Char] -> ConfigDesc
mkO [Char]
"solver.yices."
in [ ConfigDesc
f
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
f] forall a b. (a -> b) -> a -> b
$ [Char] -> ConfigDesc
mkO [Char]
"yices."
]
intWithRangeOpt :: String -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt :: [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
nm Integer
lo Integer
hi =
let mkO :: [Char] -> ConfigDesc
mkO [Char]
n = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
BaseIntegerRepr forall a b. (a -> b) -> a -> b
$ [Char]
nforall a. [a] -> [a] -> [a]
++[Char]
nm)
(Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
integerWithRangeOptSty (forall r. r -> Bound r
Inclusive Integer
lo) (forall r. r -> Bound r
Inclusive Integer
hi))
forall a. Maybe a
Nothing
forall a. Maybe a
Nothing
i :: ConfigDesc
i = [Char] -> ConfigDesc
mkO [Char]
"solver.yices."
in [ ConfigDesc
i
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
i] forall a b. (a -> b) -> a -> b
$ [Char] -> ConfigDesc
mkO [Char]
"yices."
]
enumOpt :: String -> Set Text -> [ConfigDesc]
enumOpt :: [Char] -> Set Text -> [ConfigDesc]
enumOpt [Char]
nm Set Text
xs =
let mkO :: [Char] -> ConfigDesc
mkO [Char]
n = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt (forall (tp :: BaseType).
BaseTypeRepr tp -> [Char] -> ConfigOption tp
configOption (forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr Unicode
UnicodeRepr) forall a b. (a -> b) -> a -> b
$ [Char]
nforall a. [a] -> [a] -> [a]
++[Char]
nm)
(Set Text -> OptionStyle (BaseStringType Unicode)
enumOptSty Set Text
xs)
forall a. Maybe a
Nothing
forall a. Maybe a
Nothing
e :: ConfigDesc
e = [Char] -> ConfigDesc
mkO [Char]
"solver.yices."
in [ ConfigDesc
e
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
e] forall a b. (a -> b) -> a -> b
$ [Char] -> ConfigDesc
mkO [Char]
"yices."
]
yicesInternalOptions :: [ConfigDesc]
yicesInternalOptions :: [ConfigDesc]
yicesInternalOptions = forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [ConfigDesc]
booleanOpt [Char]
"var-elim"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"arith-elim"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"flatten"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"learn-eq"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"keep-ite"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"fast-restarts"
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"c-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Bound Rational -> [ConfigDesc]
floatWithMinOpt [Char]
"c-factor" (forall r. r -> Bound r
Inclusive Rational
1)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"d-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Rational -> Rational -> [ConfigDesc]
floatWithRangeOpt [Char]
"d-factor" Rational
1 Rational
1.5
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"r-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Rational -> Rational -> [ConfigDesc]
floatWithRangeOpt [Char]
"r-fraction" Rational
0 Rational
1
, [Char] -> Bound Rational -> [ConfigDesc]
floatWithMinOpt [Char]
"r-factor" (forall r. r -> Bound r
Inclusive Rational
1)
, [Char] -> Rational -> Rational -> [ConfigDesc]
floatWithRangeOpt [Char]
"var-decay" Rational
0 Rational
1
, [Char] -> Rational -> Rational -> [ConfigDesc]
floatWithRangeOpt [Char]
"randomness" Rational
0 Rational
1
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"random-seed" (forall a. Num a => a -> a
negate (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)) (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Set Text -> [ConfigDesc]
enumOpt [Char]
"branching" Set Text
yicesBranchingChoices
, [Char] -> Rational -> Rational -> [ConfigDesc]
floatWithRangeOpt [Char]
"clause-decay" Rational
0 Rational
1
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"cache-tclauses"
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"tclause-size" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"dyn-ack"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"dyn-bool-ack"
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"max-ack" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"max-bool-ack" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"aux-eq-quota" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Bound Rational -> [ConfigDesc]
floatWithMinOpt [Char]
"aux-eq-ratio" (forall r. r -> Bound r
Exclusive Rational
0)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"dyn-ack-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
16::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"dyn-bool-ack-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
16::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"max-interface-eqs" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"eager-lemmas"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"simplex-prop"
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"prop-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"simplex-adjust"
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"bland-threshold" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"icheck"
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"icheck-period" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"max-update-conflicts" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"max-extensionality" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"bvarith-elim"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"optimistic-fcheck"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"ef-flatten-iff"
, [Char] -> [ConfigDesc]
booleanOpt [Char]
"ef-flatten-ite"
, [Char] -> Set Text -> [ConfigDesc]
enumOpt [Char]
"ef-gen-mode" Set Text
yicesEFGenModes
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"ef-max-iters" Integer
1 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [Char] -> Integer -> Integer -> [ConfigDesc]
intWithRangeOpt [Char]
"ef-max-samples" Integer
0 (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
]
checkSupportedByYices :: B.BoolExpr t -> IO ProblemFeatures
checkSupportedByYices :: forall t. BoolExpr t -> IO ProblemFeatures
checkSupportedByYices BoolExpr t
p = do
let varInfo :: CollectedVarInfo t
varInfo = forall t. Expr t BaseBoolType -> CollectedVarInfo t
predicateVarInfo BoolExpr t
p
let errors :: [Doc Void]
errors = forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (CollectedVarInfo t
varInfoforall s a. s -> Getting a s a -> a
^.forall t. Simple Lens (CollectedVarInfo t) (Seq (Doc Void))
varErrors)
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Doc Void]
errors)) forall a b. (a -> b) -> a -> b
$ do
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$
forall ann. [Doc ann] -> Doc ann
PP.vcat [Doc Void
"This formula is not supported by yices:", forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (forall ann. [Doc ann] -> Doc ann
PP.vcat [Doc Void]
errors)]
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! CollectedVarInfo t
varInfoforall s a. s -> Getting a s a -> a
^.forall t. Simple Lens (CollectedVarInfo t) ProblemFeatures
problemFeatures
writeYicesFile :: B.ExprBuilder t st fs
-> FilePath
-> B.BoolExpr t
-> IO ()
writeYicesFile :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> [Char] -> BoolExpr t -> IO ()
writeYicesFile ExprBuilder t st fs
sym [Char]
path BoolExpr t
p = do
forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
withFile [Char]
path IOMode
WriteMode forall a b. (a -> b) -> a -> b
$ \Handle
h -> do
let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
let varInfo :: CollectedVarInfo t
varInfo = forall t. Expr t BaseBoolType -> CollectedVarInfo t
predicateVarInfo BoolExpr t
p
let features :: ProblemFeatures
features = CollectedVarInfo t
varInfoforall s a. s -> Getting a s a -> a
^.forall t. Simple Lens (CollectedVarInfo t) ProblemFeatures
problemFeatures
let efSolver :: Bool
efSolver = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useExistForall
SymbolVarBimap t
bindings <- forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
B.getSymbolVarBimap ExprBuilder t st fs
sym
OutputStream Text
str <- OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
h
InputStream Text
in_str <- forall a. IO (InputStream a)
Streams.nullInput
let t :: SolverGoalTimeout
t = Integer -> SolverGoalTimeout
SolverGoalTimeout Integer
0
WriterConn t Connection
c <- forall t.
OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
newConnection OutputStream Text
str InputStream Text
in_str (forall a b. a -> b -> a
const forall t h. AcknowledgementAction t h
nullAcknowledgementAction) ProblemFeatures
features SolverGoalTimeout
t SymbolVarBimap t
bindings
forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
c Config
cfg
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn t Connection
c BoolExpr t
p
if Bool
efSolver then
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c Command Connection
efSolveCommand
else
forall t. WriterConn t Connection -> IO ()
sendCheck WriterConn t Connection
c
forall t. WriterConn t Connection -> IO ()
sendShowModel WriterConn t Connection
c
runYicesInOverride :: B.ExprBuilder t st fs
-> LogData
-> [B.BoolExpr t]
-> (SatResult (GroundEvalFn t) () -> IO a)
-> IO a
runYicesInOverride :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t) () -> IO a)
-> IO a
runYicesInOverride ExprBuilder t st fs
sym LogData
logData [BoolExpr t]
conditions SatResult (GroundEvalFn t) () -> IO a
resultFn = do
let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
[Char]
yices_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
findSolverPath ConfigOption (BaseStringType Unicode)
yicesPath Config
cfg
BoolExpr t
condition <- forall sym s.
IsExprBuilder sym =>
sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
andAllOf ExprBuilder t st fs
sym forall (f :: Type -> Type) a. Foldable f => IndexedFold Int (f a) a
folded [BoolExpr t]
conditions
LogData -> Int -> [Char] -> IO ()
logCallbackVerbose LogData
logData Int
2 [Char]
"Calling Yices to check sat"
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
(SolverStartSATQuery -> SolverEvent
SolverStartSATQuery forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec
{ satQuerySolverName :: [Char]
satQuerySolverName = [Char]
"Yices"
, satQueryReason :: [Char]
satQueryReason = LogData -> [Char]
logReason LogData
logData
})
ProblemFeatures
features <- forall t. BoolExpr t -> IO ProblemFeatures
checkSupportedByYices BoolExpr t
condition
Bool
enableMCSat <- forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
yicesEnableMCSat Config
cfg
SolverGoalTimeout
goalTimeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
yicesGoalTimeout Config
cfg)
let efSolver :: Bool
efSolver = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useExistForall
let nlSolver :: Bool
nlSolver = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useNonlinearArithmetic
let args0 :: [[Char]]
args0 | Bool
efSolver = [[Char]
"--mode=ef"]
| Bool
nlSolver = [[Char]
"--logic=QF_NRA"]
| Bool
otherwise = [[Char]
"--mode=one-shot"]
let args :: [[Char]]
args = [[Char]]
args0 forall a. [a] -> [a] -> [a]
++ if Bool
enableMCSat then [[Char]
"--mcsat"] else []
hasNamedAssumptions :: Bool
hasNamedAssumptions = ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores Bool -> Bool -> Bool
||
ProblemFeatures
features ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatAssumptions
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
enableMCSat Bool -> Bool -> Bool
&& Bool
hasNamedAssumptions) forall a b. (a -> b) -> a -> b
$
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Unsat cores and named assumptions are incompatible with MC-SAT in Yices."
forall a.
[Char]
-> [[Char]]
-> Maybe [Char]
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
withProcessHandles [Char]
yices_path [[Char]]
args forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \hdls :: (Handle, Handle, Handle, ProcessHandle)
hdls@(Handle
in_h, Handle
out_h, Handle
err_h, ProcessHandle
ph) -> do
(OutputStream Text
in_stream, InputStream Text
out_stream, HandleReader
err_reader) <-
Handle
-> Handle
-> Handle
-> Maybe (Text, Handle)
-> IO (OutputStream Text, InputStream Text, HandleReader)
demuxProcessHandles Handle
in_h Handle
out_h Handle
err_h
(forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Handle
x -> (Text
"; ",Handle
x)) forall a b. (a -> b) -> a -> b
$ LogData -> Maybe Handle
logHandle LogData
logData)
SymbolVarBimap t
bindings <- forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
B.getSymbolVarBimap ExprBuilder t st fs
sym
WriterConn t Connection
c <- forall t.
OutputStream Text
-> InputStream Text
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection)
-> ProblemFeatures
-> SolverGoalTimeout
-> SymbolVarBimap t
-> IO (WriterConn t Connection)
newConnection OutputStream Text
in_stream InputStream Text
out_stream (forall a b. a -> b -> a
const forall t h. AcknowledgementAction t h
nullAcknowledgementAction) ProblemFeatures
features SolverGoalTimeout
goalTimeout SymbolVarBimap t
bindings
forall t. WriterConn t Connection -> Config -> IO ()
setYicesParams WriterConn t Connection
c Config
cfg
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn t Connection
c BoolExpr t
condition
LogData -> Int -> [Char] -> IO ()
logCallbackVerbose LogData
logData Int
2 [Char]
"Running check sat"
if Bool
efSolver then
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t Connection
c Command Connection
efSolveCommand
else
forall t. WriterConn t Connection -> IO ()
sendCheck WriterConn t Connection
c
let yp :: SolverProcess t Connection
yp = SolverProcess { solverConn :: WriterConn t Connection
solverConn = WriterConn t Connection
c
, solverCleanupCallback :: IO ExitCode
solverCleanupCallback = (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
cleanupProcess (Handle, Handle, Handle, ProcessHandle)
hdls
, solverHandle :: ProcessHandle
solverHandle = ProcessHandle
ph
, solverErrorBehavior :: ErrorBehavior
solverErrorBehavior = ErrorBehavior
ImmediateExit
, solverStderr :: HandleReader
solverStderr = HandleReader
err_reader
, solverEvalFuns :: SMTEvalFunctions Connection
solverEvalFuns = forall h t.
SMTReadWriter h =>
WriterConn t h -> InputStream Text -> SMTEvalFunctions h
smtEvalFuns WriterConn t Connection
c InputStream Text
out_stream
, solverName :: [Char]
solverName = [Char]
"Yices"
, solverLogFn :: SolverEvent -> IO ()
solverLogFn = forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
, solverEarlyUnsat :: IORef (Maybe Int)
solverEarlyUnsat = Connection -> IORef (Maybe Int)
yicesEarlyUnsat (forall t h. WriterConn t h -> h
connState WriterConn t Connection
c)
, solverSupportsResetAssertions :: Bool
solverSupportsResetAssertions = Bool
True
, solverGoalTimeout :: SolverGoalTimeout
solverGoalTimeout = SolverGoalTimeout
goalTimeout
}
SatResult () ()
sat_result <- forall s t.
SMTReadWriter s =>
SolverProcess t s -> IO (SatResult () ())
getSatResult SolverProcess t Connection
yp
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
(SolverEndSATQuery -> SolverEvent
SolverEndSATQuery forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
{ satQueryResult :: SatResult () ()
satQueryResult = SatResult () ()
sat_result
, satQueryError :: Maybe [Char]
satQueryError = forall a. Maybe a
Nothing
})
a
r <-
case SatResult () ()
sat_result of
Sat () -> SatResult (GroundEvalFn t) () -> IO a
resultFn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall mdl core. mdl -> SatResult mdl core
Sat forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel SolverProcess t Connection
yp
Unsat ()
x -> SatResult (GroundEvalFn t) () -> IO a
resultFn (forall mdl core. core -> SatResult mdl core
Unsat ()
x)
SatResult () ()
Unknown -> SatResult (GroundEvalFn t) () -> IO a
resultFn forall mdl core. SatResult mdl core
Unknown
(ExitCode, Text)
_ <- forall scope. SolverProcess scope Connection -> IO (ExitCode, Text)
yicesShutdownSolver SolverProcess t Connection
yp
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
r