------------------------------------------------------------------------
-- |
-- Module      : What4.Solver.Z3
-- Description : Solver adapter code for Z3
-- Copyright   : (c) Galois, Inc 2015-2020
-- License     : BSD3
-- Maintainer  : Rob Dockins <rdockins@galois.com>
-- Stability   : provisional
--
-- Z3-specific tweaks to the basic SMTLib2 solver interface.
------------------------------------------------------------------------
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
module What4.Solver.Z3
  ( Z3(..)
  , z3Adapter
  , z3Path
  , z3Timeout
  , z3Options
  , z3Tactic
  , z3TacticDefault
  , z3Features
  , runZ3InOverride
  , withZ3
  , writeZ3SMT2File
  , runZ3Horn
  , writeZ3HornSMT2File
  ) where

import           Control.Monad ( when )
import qualified Data.Bimap as Bimap
import           Data.Bits
import           Data.Foldable
import           Data.Map.Strict (Map)
import qualified Data.Map as Map
import           Data.String
import           Data.Text (Text)
import qualified Data.Text as T
import           System.IO

import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.Some
import           What4.BaseTypes
import           What4.Concrete
import           What4.Config
import           What4.Expr.Builder
import           What4.Expr.GroundEval
import           What4.Interface
import           What4.ProblemFeatures
import           What4.Protocol.Online
import qualified What4.Protocol.SMTLib2 as SMT2
import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
import qualified What4.Protocol.SMTLib2.Response as RSP
import qualified What4.Protocol.SMTLib2.Syntax as Syntax
import           What4.Protocol.SMTWriter
import           What4.SatResult
import           What4.Solver.Adapter
import           What4.Utils.Process

data Z3 = Z3 deriving Int -> Z3 -> ShowS
[Z3] -> ShowS
Z3 -> String
(Int -> Z3 -> ShowS)
-> (Z3 -> String) -> ([Z3] -> ShowS) -> Show Z3
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Z3 -> ShowS
showsPrec :: Int -> Z3 -> ShowS
$cshow :: Z3 -> String
show :: Z3 -> String
$cshowList :: [Z3] -> ShowS
showList :: [Z3] -> ShowS
Show

-- | Path to Z3
z3Path :: ConfigOption (BaseStringType Unicode)
z3Path :: ConfigOption (BaseStringType Unicode)
z3Path = BaseTypeRepr (BaseStringType Unicode)
-> String -> ConfigOption (BaseStringType Unicode)
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr (BaseStringType Unicode)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.z3.path"

z3PathOLD :: ConfigOption (BaseStringType Unicode)
z3PathOLD :: ConfigOption (BaseStringType Unicode)
z3PathOLD = BaseTypeRepr (BaseStringType Unicode)
-> String -> ConfigOption (BaseStringType Unicode)
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr (BaseStringType Unicode)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"z3_path"

-- | Per-check timeout, in milliseconds (zero is none)
z3Timeout :: ConfigOption BaseIntegerType
z3Timeout :: ConfigOption BaseIntegerType
z3Timeout = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.z3.timeout"

z3TimeoutOLD :: ConfigOption BaseIntegerType
z3TimeoutOLD :: ConfigOption BaseIntegerType
z3TimeoutOLD = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"z3_timeout"
-- | Strict parsing specifically for Z3 interaction?  If set,
-- overrides solver.strict_parsing, otherwise defaults to
-- solver.strict_parsing.
z3StrictParsing  :: ConfigOption BaseBoolType
z3StrictParsing :: ConfigOption BaseBoolType
z3StrictParsing = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.z3.strict_parsing"

-- | Z3 tactic
z3Tactic :: ConfigOption (BaseStringType Unicode)
z3Tactic :: ConfigOption (BaseStringType Unicode)
z3Tactic = BaseTypeRepr (BaseStringType Unicode)
-> String -> ConfigOption (BaseStringType Unicode)
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr (BaseStringType Unicode)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.z3.tactic"

z3TacticDefault :: Text
z3TacticDefault :: Text
z3TacticDefault = Text
""

z3Options :: [ConfigDesc]
z3Options :: [ConfigDesc]
z3Options =
  let mkPath :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
co = ConfigOption (BaseStringType Unicode)
-> OptionStyle (BaseStringType Unicode)
-> Maybe (Doc Void)
-> Maybe (ConcreteVal (BaseStringType Unicode))
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption (BaseStringType Unicode)
co
                  OptionStyle (BaseStringType Unicode)
executablePathOptSty
                  (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Z3 executable path")
                  (ConcreteVal (BaseStringType Unicode)
-> Maybe (ConcreteVal (BaseStringType Unicode))
forall a. a -> Maybe a
Just (StringLiteral Unicode -> ConcreteVal (BaseStringType Unicode)
forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString StringLiteral Unicode
"z3"))
      mkTmo :: ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
co = ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
co
                 OptionStyle BaseIntegerType
integerOptSty
                 (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Per-check timeout in milliseconds (zero is none)")
                 (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
0))
      p :: ConfigDesc
p = ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
z3Path
      t :: ConfigDesc
t = ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
z3Timeout
  in [ ConfigDesc
p, ConfigDesc
t
     , (Text -> Text) -> ConfigDesc -> ConfigDesc
copyOpt (Text -> Text -> Text
forall a b. a -> b -> a
const (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. (a -> b) -> a -> b
$ ConfigOption BaseBoolType -> Text
forall (tp :: BaseType). ConfigOption tp -> Text
configOptionText ConfigOption BaseBoolType
z3StrictParsing) ConfigDesc
strictSMTParseOpt
     , ConfigOption (BaseStringType Unicode)
-> OptionStyle (BaseStringType Unicode)
-> Maybe (Doc Void)
-> Maybe (ConcreteVal (BaseStringType Unicode))
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption (BaseStringType Unicode)
z3Tactic OptionStyle (BaseStringType Unicode)
stringOptSty (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Z3 tactic") (ConcreteVal (BaseStringType Unicode)
-> Maybe (ConcreteVal (BaseStringType Unicode))
forall a. a -> Maybe a
Just (StringLiteral Unicode -> ConcreteVal (BaseStringType Unicode)
forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString (Text -> StringLiteral Unicode
UnicodeLiteral Text
z3TacticDefault)))
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
p] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
z3PathOLD
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
t] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
forall a b. (a -> b) -> a -> b
$ ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
z3TimeoutOLD
     ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options

z3Adapter :: SolverAdapter st
z3Adapter :: forall (st :: Type -> Type). SolverAdapter st
z3Adapter =
  SolverAdapter
  { solver_adapter_name :: String
solver_adapter_name = String
"z3"
  , solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
z3Options
  , solver_adapter_check_sat :: forall t fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
solver_adapter_check_sat = ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
forall t fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runZ3InOverride
  , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 = ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeZ3SMT2File
  }

indexType :: [SMT2.Sort] -> SMT2.Sort
indexType :: [Sort] -> Sort
indexType [Sort
i] = Sort
i
indexType [Sort]
il = forall a. SMTLib2Tweaks a => [Sort] -> Sort
SMT2.smtlib2StructSort @Z3 [Sort]
il

indexCtor :: [SMT2.Term] -> SMT2.Term
indexCtor :: [Term] -> Term
indexCtor [Term
i] = Term
i
indexCtor [Term]
il = forall a. SMTLib2Tweaks a => [Term] -> Term
SMT2.smtlib2StructCtor @Z3 [Term]
il

instance SMT2.SMTLib2Tweaks Z3 where
  smtlib2tweaks :: Z3
smtlib2tweaks = Z3
Z3

  smtlib2arrayType :: [Sort] -> Sort -> Sort
smtlib2arrayType [Sort]
il Sort
r = Sort -> Sort -> Sort
SMT2.arraySort ([Sort] -> Sort
indexType [Sort]
il) Sort
r

  smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)
smtlib2arrayConstant = ([Sort] -> Sort -> Term -> Term)
-> Maybe ([Sort] -> Sort -> Term -> Term)
forall a. a -> Maybe a
Just (([Sort] -> Sort -> Term -> Term)
 -> Maybe ([Sort] -> Sort -> Term -> Term))
-> ([Sort] -> Sort -> Term -> Term)
-> Maybe ([Sort] -> Sort -> Term -> Term)
forall a b. (a -> b) -> a -> b
$ \[Sort]
idx Sort
rtp Term
v ->
    Sort -> Sort -> Term -> Term
SMT2.arrayConst ([Sort] -> Sort
indexType [Sort]
idx) Sort
rtp Term
v
  smtlib2arraySelect :: Term -> [Term] -> Term
smtlib2arraySelect Term
a [Term]
i = Term -> Term -> Term
SMT2.arraySelect Term
a ([Term] -> Term
indexCtor [Term]
i)
  smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term
smtlib2arrayUpdate Term
a [Term]
i = Term -> Term -> Term -> Term
SMT2.arrayStore Term
a ([Term] -> Term
indexCtor [Term]
i)

  -- Z3 uses a datatype declaration command that differs from the
  -- SMTLib 2.6 standard
  smtlib2declareStructCmd :: Int -> Maybe Command
smtlib2declareStructCmd Int
n = Command -> Maybe Command
forall a. a -> Maybe a
Just (Command -> Maybe Command) -> Command -> Maybe Command
forall a b. (a -> b) -> a -> b
$
      let type_name :: a -> a
type_name a
i = String -> a
forall a. IsString a => String -> a
fromString (Char
'T' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show (a
ia -> a -> a
forall a. Num a => a -> a -> a
-a
1))
          params :: Builder
params = [Builder] -> Builder
builder_list ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ Int -> Builder
forall {a} {a}. (IsString a, Show a, Num a) => a -> a
type_name  (Int -> Builder) -> [Int] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
n]
          n_str :: Builder
n_str = String -> Builder
forall a. IsString a => String -> a
fromString (Int -> String
forall a. Show a => a -> String
show Int
n)
          tp :: Builder
tp = Builder
"Struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str
          ctor :: Builder
ctor = Builder
"mk-struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str
          field_def :: Int -> Builder
field_def Int
i = Builder -> [Builder] -> Builder
app Builder
field_nm [Int -> Builder
forall {a} {a}. (IsString a, Show a, Num a) => a -> a
type_name Int
i]
            where field_nm :: Builder
field_nm = Builder
"struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"-proj" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. IsString a => String -> a
fromString (Int -> String
forall a. Show a => a -> String
show (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
          fields :: [Builder]
fields = Int -> Builder
field_def (Int -> Builder) -> [Int] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
n]
          decl :: Builder
decl = Builder -> [Builder] -> Builder
app Builder
tp [Builder -> [Builder] -> Builder
app Builder
ctor [Builder]
fields]
          decls :: Builder
decls = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
decl Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
       in Builder -> Command
Syntax.Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-datatypes" [ Builder
params, Builder
decls ]

z3Features :: ProblemFeatures
z3Features :: ProblemFeatures
z3Features = ProblemFeatures
useNonlinearArithmetic
         ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
         ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
         ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useSymbolicArrays
         ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStructs
         ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStrings
         ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useFloatingPoint
         ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors

writeZ3SMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeZ3SMT2File :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeZ3SMT2File = Z3
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
SMT2.writeDefaultSMT2 Z3
Z3 String
"Z3" ProblemFeatures
z3Features (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)

instance SMT2.SMTLib2GenericSolver Z3 where
  defaultSolverPath :: forall t (st :: Type -> Type) fs.
Z3 -> ExprBuilder t st fs -> IO String
defaultSolverPath Z3
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
z3Path (Config -> IO String)
-> (ExprBuilder t st fs -> Config)
-> ExprBuilder t st fs
-> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration

  defaultSolverArgs :: forall t (st :: Type -> Type) fs.
Z3 -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs Z3
_ ExprBuilder t st fs
sym = do
    let cfg :: Config
cfg = ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
    Maybe (ConcreteVal BaseIntegerType)
timeout <- OptionSetting BaseIntegerType
-> IO (Maybe (ConcreteVal BaseIntegerType))
forall (tp :: BaseType).
OptionSetting tp -> IO (Maybe (ConcreteVal tp))
getOption (OptionSetting BaseIntegerType
 -> IO (Maybe (ConcreteVal BaseIntegerType)))
-> IO (OptionSetting BaseIntegerType)
-> IO (Maybe (ConcreteVal BaseIntegerType))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
z3Timeout Config
cfg
    let extraOpts :: [String]
extraOpts = case Maybe (ConcreteVal BaseIntegerType)
timeout of
                      Just (ConcreteInteger Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> [String
"-t:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n]
                      Maybe (ConcreteVal BaseIntegerType)
_ -> []
    Text
tactic <- OptionSetting (BaseStringType Unicode) -> IO Text
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting (BaseStringType Unicode) -> IO Text)
-> IO (OptionSetting (BaseStringType Unicode)) -> IO Text
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption (BaseStringType Unicode)
-> Config -> IO (OptionSetting (BaseStringType Unicode))
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption (BaseStringType Unicode)
z3Tactic Config
cfg
    let tacticOpt :: [String]
tacticOpt = if Text
tactic Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Text
z3TacticDefault then [String
"tactic.default_tactic=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
tactic] else []
    [String] -> IO [String]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ [String]
tacticOpt [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"-smt2", String
"-in"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extraOpts

  getErrorBehavior :: forall t. Z3 -> WriterConn t (Writer Z3) -> IO ErrorBehavior
getErrorBehavior Z3
_ = WriterConn t (Writer Z3) -> IO ErrorBehavior
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> IO ErrorBehavior
SMT2.queryErrorBehavior

  defaultFeatures :: Z3 -> ProblemFeatures
defaultFeatures Z3
_ = ProblemFeatures
z3Features

  supportsResetAssertions :: Z3 -> Bool
supportsResetAssertions Z3
_ = Bool
True

  setDefaultLogicAndOptions :: forall t. WriterConn t (Writer Z3) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer Z3)
writer = do
    -- Tell Z3 to produce models.
    WriterConn t (Writer Z3) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer Z3)
writer Text
"produce-models" Text
"true"
    -- Tell Z3 to round and print algebraic reals as decimal
    WriterConn t (Writer Z3) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer Z3)
writer Text
"pp.decimal" Text
"true"
    -- Tell Z3 to compute UNSAT cores, if that feature is enabled
    Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (WriterConn t (Writer Z3) -> ProblemFeatures
forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn t (Writer Z3)
writer ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
      WriterConn t (Writer Z3) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer Z3)
writer Text
"produce-unsat-cores" Text
"true"

runZ3InOverride
  :: ExprBuilder t st fs
  -> LogData
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
runZ3InOverride :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runZ3InOverride = Z3
-> AcknowledgementAction t (Writer Z3)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
forall t (st :: Type -> Type) fs b.
Z3
-> AcknowledgementAction t (Writer Z3)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
SMT2.runSolverInOverride Z3
Z3 AcknowledgementAction t (Writer Z3)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction
                  ProblemFeatures
z3Features (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)

-- | Run Z3 in a session. Z3 will be configured to produce models, but
-- otherwise left with the default configuration.
withZ3
  :: ExprBuilder t st fs
  -> FilePath
    -- ^ Path to Z3 executable
  -> LogData
  -> (SMT2.Session t Z3 -> IO a)
    -- ^ Action to run
  -> IO a
withZ3 :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t Z3 -> IO a) -> IO a
withZ3 = Z3
-> AcknowledgementAction t (Writer Z3)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t Z3 -> IO a)
-> IO a
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
forall t (st :: Type -> Type) fs b.
Z3
-> AcknowledgementAction t (Writer Z3)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t Z3 -> IO b)
-> IO b
SMT2.withSolver Z3
Z3 AcknowledgementAction t (Writer Z3)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction
         ProblemFeatures
z3Features (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)


setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions WriterConn t (Writer a)
writer = do
    -- Tell Z3 to acknowledge successful commands
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"print-success"  Text
"true"
    -- Tell Z3 to produce models
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-models" Text
"true"
    -- Tell Z3 to round and print algebraic reals as decimal
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"pp.decimal" Text
"true"
    -- Tell Z3 to make declarations global, so they are not removed by 'pop' commands
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"global-declarations" Text
"true"
    -- Tell Z3 to compute UNSAT cores, if that feature is enabled
    Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (WriterConn t (Writer a) -> ProblemFeatures
forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn t (Writer a)
writer ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-unsat-cores" Text
"true"

instance OnlineSolver (SMT2.Writer Z3) where

  startSolverProcess :: forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Z3))
startSolverProcess ProblemFeatures
feat Maybe Handle
mbIOh ExprBuilder scope st fs
sym = do
    SolverGoalTimeout
timeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout (Integer -> SolverGoalTimeout)
-> IO Integer -> IO SolverGoalTimeout
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
               (OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseIntegerType -> IO Integer)
-> IO (OptionSetting BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
z3Timeout (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym))
    Z3
-> AcknowledgementAction scope (Writer Z3)
-> (WriterConn scope (Writer Z3) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Z3))
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> (WriterConn t (Writer a) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder t st fs
-> IO (SolverProcess t (Writer a))
SMT2.startSolver Z3
Z3 AcknowledgementAction scope (Writer Z3)
forall t a. AcknowledgementAction t (Writer a)
SMT2.smtAckResult WriterConn scope (Writer Z3) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions
      SolverGoalTimeout
timeout ProblemFeatures
feat (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing) Maybe Handle
mbIOh ExprBuilder scope st fs
sym

  shutdownSolverProcess :: forall scope.
SolverProcess scope (Writer Z3) -> IO (ExitCode, Text)
shutdownSolverProcess = Z3 -> SolverProcess scope (Writer Z3) -> IO (ExitCode, Text)
forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver Z3
Z3

-- | Check the satisfiability of a set of constrained Horn clauses (CHCs).
--
-- CHCs are represented as pure SMT-LIB2 implications. For more information, see
-- the [Z3 guide](https://microsoft.github.io/z3guide/docs/fixedpoints/intro/).
--
-- There are two ways to solve the CHCs: either by directly solving the problem
-- as is, or by transforming the problem into a set of linear integer arithmetic
-- (LIA) CHCs and solving that instead. The latter is done by replacing all
-- bitvector (BV) operations with LIA operations, and replacing all BV variables
-- with LIA variables. This transformation is not sound, but in practice it is a
-- useful heuristic. Then the result is transformed back into a BV result, and
-- checked for satisfiability. The satisfiability check is necessary because the
-- transformation is not sound, so LIA solution may not be a solution to the BV
-- CHCs.
runZ3Horn ::
  forall sym t st fs .
  sym ~ ExprBuilder t st fs =>
  sym ->
  Bool {- transform the BV CHCs into LIA CHCs -} ->
  LogData ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
runZ3Horn :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Bool
-> LogData
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
runZ3Horn sym
sym Bool
do_bv_to_lia_transform LogData
log_data [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses = do
  ([SomeSymFn sym]
lia_inv_fns, [BoolExpr t]
lia_horn_clauses, Map (SomeSymFn sym) (SomeSymFn sym)
bv_to_lia_fn_subst) <- sym
-> Bool
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO
     ([SomeSymFn sym], [BoolExpr t],
      Map (SomeSymFn sym) (SomeSymFn sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Bool
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO
     ([SomeSymFn sym], [BoolExpr t],
      Map (SomeSymFn sym) (SomeSymFn sym))
transformHornClausesForZ3
    sym
sym
    Bool
do_bv_to_lia_transform
    [SomeSymFn sym]
inv_fns
    [BoolExpr t]
horn_clauses

  sym -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent sym
sym
    (SolverStartSATQuery -> SolverEvent
SolverStartSATQuery (SolverStartSATQuery -> SolverEvent)
-> SolverStartSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec
      { satQuerySolverName :: String
satQuerySolverName = Z3 -> String
forall a. Show a => a -> String
show Z3
Z3
      , satQueryReason :: String
satQueryReason = LogData -> String
logReason LogData
log_data
      })

  String
path <- Z3 -> ExprBuilder t st fs -> IO String
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO String
forall t (st :: Type -> Type) fs.
Z3 -> ExprBuilder t st fs -> IO String
SMT2.defaultSolverPath Z3
Z3 sym
ExprBuilder t st fs
sym
  SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
get_value_result <- ExprBuilder t st fs
-> String
-> LogData
-> (Session t Z3
    -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t Z3 -> IO a) -> IO a
withZ3 sym
ExprBuilder t st fs
sym String
path (LogData
log_data { logVerbosity = 2 }) ((Session t Z3
  -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
 -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
-> (Session t Z3
    -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall a b. (a -> b) -> a -> b
$ \Session t Z3
session -> do
    sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeHornProblem sym
sym (Session t Z3 -> WriterConn t (Writer Z3)
forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t Z3
session) [SomeSymFn sym]
lia_inv_fns [BoolExpr t]
lia_horn_clauses

    SatResult () ()
check_sat_result <- String
-> (SMTResponse -> Maybe (SatResult () ()))
-> WriterConn t (Writer Z3)
-> Command
-> IO (SatResult () ())
forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
RSP.getLimitedSolverResponse String
"check-sat"
      (\case
        SMTResponse
RSP.AckSat -> SatResult () () -> Maybe (SatResult () ())
forall a. a -> Maybe a
Just (SatResult () () -> Maybe (SatResult () ()))
-> SatResult () () -> Maybe (SatResult () ())
forall a b. (a -> b) -> a -> b
$ () -> SatResult () ()
forall mdl core. mdl -> SatResult mdl core
Sat ()
        SMTResponse
RSP.AckUnsat -> SatResult () () -> Maybe (SatResult () ())
forall a. a -> Maybe a
Just (SatResult () () -> Maybe (SatResult () ()))
-> SatResult () () -> Maybe (SatResult () ())
forall a b. (a -> b) -> a -> b
$ () -> SatResult () ()
forall mdl core. core -> SatResult mdl core
Unsat ()
        SMTResponse
RSP.AckUnknown -> SatResult () () -> Maybe (SatResult () ())
forall a. a -> Maybe a
Just SatResult () ()
forall mdl core. SatResult mdl core
Unknown
        SMTResponse
_ -> Maybe (SatResult () ())
forall a. Maybe a
Nothing)
      (Session t Z3 -> WriterConn t (Writer Z3)
forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t Z3
session)
      Command
Syntax.checkSat

    sym -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent sym
sym
      (SolverEndSATQuery -> SolverEvent
SolverEndSATQuery (SolverEndSATQuery -> SolverEvent)
-> SolverEndSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
        { satQueryResult :: SatResult () ()
satQueryResult = SatResult () ()
check_sat_result
        , satQueryError :: Maybe String
satQueryError = Maybe String
forall a. Maybe a
Nothing
        })

    (() -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)))
-> (() -> IO ())
-> SatResult () ()
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall (t :: Type -> Type) a q b r.
Applicative t =>
(a -> t q) -> (b -> t r) -> SatResult a b -> t (SatResult q r)
traverseSatResult
      (\() -> do
        SExp
sexp <- String
-> (SMTResponse -> Maybe SExp)
-> WriterConn t (Writer Z3)
-> Command
-> IO SExp
forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
RSP.getLimitedSolverResponse String
"get-value"
          (\case
            RSP.AckSuccessSExp SExp
sexp -> SExp -> Maybe SExp
forall a. a -> Maybe a
Just SExp
sexp
            SMTResponse
_ -> Maybe SExp
forall a. Maybe a
Nothing)
          (Session t Z3 -> WriterConn t (Writer Z3)
forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t Z3
session)
          ([Term] -> Command
Syntax.getValue [])
        sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall sym t (st :: Type -> Type) fs h.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t h
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
SMT2.parseFnValues sym
sym (Session t Z3 -> WriterConn t (Writer Z3)
forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t Z3
session) [SomeSymFn sym]
lia_inv_fns SExp
sexp)
      () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return
      SatResult () ()
check_sat_result

  let transform_result_lia_to_bv ::
        SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) () ->
        IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
      transform_result_lia_to_bv :: SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
transform_result_lia_to_bv = \case
        Sat MapF (SymFnWrapper sym) (SymFnWrapper sym)
lia_defined_fns -> do
          MapF (SymFnWrapper sym) (SymFnWrapper sym)
defined_inv_fns <- [Pair (SymFnWrapper sym) (SymFnWrapper sym)]
-> MapF (SymFnWrapper sym) (SymFnWrapper sym)
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
[Pair k a] -> MapF k a
MapF.fromList ([Pair (SymFnWrapper sym) (SymFnWrapper sym)]
 -> MapF (SymFnWrapper sym) (SymFnWrapper sym))
-> IO [Pair (SymFnWrapper sym) (SymFnWrapper sym)]
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (SomeSymFn sym -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym)))
-> [SomeSymFn sym]
-> IO [Pair (SymFnWrapper sym) (SymFnWrapper sym)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM
            (\(SomeSymFn SymFn sym args ret
fn) ->
              if| Just (SomeSymFn SymFn sym args ret
lia_fn) <- SomeSymFn sym
-> Map (SomeSymFn sym) (SomeSymFn sym) -> Maybe (SomeSymFn sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SymFn sym args ret -> SomeSymFn sym
forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SomeSymFn sym
SomeSymFn SymFn sym args ret
fn) Map (SomeSymFn sym) (SomeSymFn sym)
bv_to_lia_fn_subst
                , Just (SymFnWrapper SymFn sym args ret
lia_defined_fn) <- SymFnWrapper sym (args '::> ret)
-> MapF (SymFnWrapper sym) (SymFnWrapper sym)
-> Maybe (SymFnWrapper sym (args '::> ret))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
SymFnWrapper SymFn sym args ret
lia_fn) MapF (SymFnWrapper sym) (SymFnWrapper sym)
lia_defined_fns -> do
                  SomeSymFn sym
some_defined_fn <- sym -> SomeSymFn sym -> IO (SomeSymFn sym)
forall sym.
IsSymExprBuilder sym =>
sym -> SomeSymFn sym -> IO (SomeSymFn sym)
transformSymFnLIA2BV sym
sym (SomeSymFn sym -> IO (SomeSymFn sym))
-> SomeSymFn sym -> IO (SomeSymFn sym)
forall a b. (a -> b) -> a -> b
$ SymFn sym args ret -> SomeSymFn sym
forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SomeSymFn sym
SomeSymFn SymFn sym args ret
SymFn sym args ret
lia_defined_fn
                  case SomeSymFn sym
some_defined_fn of
                    SomeSymFn SymFn sym args ret
defined_fn
                      | Just args :~: args
Refl <- Assignment BaseTypeRepr args
-> Assignment BaseTypeRepr args -> Maybe (args :~: args)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx BaseType) (b :: Ctx BaseType).
Assignment BaseTypeRepr a
-> Assignment BaseTypeRepr b -> Maybe (a :~: b)
testEquality (ExprSymFn t args ret -> Assignment BaseTypeRepr args
forall (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Assignment BaseTypeRepr args
forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
fnArgTypes SymFn sym args ret
ExprSymFn t args ret
fn) (ExprSymFn t args ret -> Assignment BaseTypeRepr args
forall (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Assignment BaseTypeRepr args
forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
fnArgTypes SymFn sym args ret
ExprSymFn t args ret
defined_fn)
                      , Just ret :~: ret
Refl <- BaseTypeRepr ret -> BaseTypeRepr ret -> Maybe (ret :~: ret)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
testEquality (ExprSymFn t args ret -> BaseTypeRepr ret
forall (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> BaseTypeRepr ret
forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
fnReturnType SymFn sym args ret
ExprSymFn t args ret
fn) (ExprSymFn t args ret -> BaseTypeRepr ret
forall (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> BaseTypeRepr ret
forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
fnReturnType SymFn sym args ret
ExprSymFn t args ret
defined_fn) ->
                        Pair (SymFnWrapper sym) (SymFnWrapper sym)
-> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pair (SymFnWrapper sym) (SymFnWrapper sym)
 -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym)))
-> Pair (SymFnWrapper sym) (SymFnWrapper sym)
-> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
forall a b. (a -> b) -> a -> b
$ SymFnWrapper sym (args '::> ret)
-> SymFnWrapper sym (args '::> ret)
-> Pair (SymFnWrapper sym) (SymFnWrapper sym)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
MapF.Pair (SymFn (ExprBuilder t st fs) args ret
-> SymFnWrapper (ExprBuilder t st fs) (args '::> ret)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
SymFnWrapper SymFn sym args ret
SymFn (ExprBuilder t st fs) args ret
fn) (SymFn (ExprBuilder t st fs) args ret
-> SymFnWrapper (ExprBuilder t st fs) (args '::> ret)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
SymFnWrapper SymFn sym args ret
SymFn (ExprBuilder t st fs) args ret
defined_fn)
                    SomeSymFn sym
_ -> String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym)))
-> String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
forall a b. (a -> b) -> a -> b
$ String
"runZ3Horn: function type mismatch in solver result: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExprSymFn t args ret -> String
forall a. Show a => a -> String
show SymFn sym args ret
ExprSymFn t args ret
fn
                | Bool
otherwise -> String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym)))
-> String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
forall a b. (a -> b) -> a -> b
$ String
"runZ3Horn: function not found in solver result: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExprSymFn t args ret -> String
forall a. Show a => a -> String
show SymFn sym args ret
ExprSymFn t args ret
fn)
            [SomeSymFn sym]
inv_fns

          Bool
all_unsat <- [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> IO [Bool] -> IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BoolExpr t -> IO Bool) -> [BoolExpr t] -> IO [Bool]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM
            (\BoolExpr t
clause -> do
              BoolExpr t
defined_clause <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (BoolExpr t -> IO (BoolExpr t))
-> IO (BoolExpr t) -> IO (BoolExpr t)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> MapF (SymFnWrapper sym) (SymFnWrapper sym)
-> Pred sym
-> IO (Pred sym)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> MapF (SymFnWrapper sym) (SymFnWrapper sym)
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym
-> MapF (SymFnWrapper sym) (SymFnWrapper sym)
-> SymExpr sym tp
-> IO (SymExpr sym tp)
substituteSymFns sym
sym MapF (SymFnWrapper sym) (SymFnWrapper sym)
defined_inv_fns Pred sym
BoolExpr t
clause
              ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO Bool)
-> IO Bool
forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runZ3InOverride sym
ExprBuilder t st fs
sym (LogData
log_data { logVerbosity = 2 }) [BoolExpr t
defined_clause] ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO Bool)
 -> IO Bool)
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO Bool)
-> IO Bool
forall a b. (a -> b) -> a -> b
$ Bool -> IO Bool
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> IO Bool)
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> Bool)
-> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> Bool
forall mdl core. SatResult mdl core -> Bool
isUnsat)
            [BoolExpr t]
horn_clauses

          SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
 -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
-> SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall a b. (a -> b) -> a -> b
$ if Bool
all_unsat then MapF (SymFnWrapper sym) (SymFnWrapper sym)
-> SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
forall mdl core. mdl -> SatResult mdl core
Sat MapF (SymFnWrapper sym) (SymFnWrapper sym)
defined_inv_fns else SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
forall mdl core. SatResult mdl core
Unknown

        SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
_ -> SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
forall mdl core. SatResult mdl core
Unknown

  if Bool
do_bv_to_lia_transform then
    SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
transform_result_lia_to_bv SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
get_value_result
  else
    SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
get_value_result

writeZ3HornSMT2File ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  Bool {- transform the BV CHCs into LIA CHCs -} ->
  Handle ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ()
writeZ3HornSMT2File :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> Bool -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()
writeZ3HornSMT2File sym
sym Bool
do_bv_to_lia_transform Handle
h [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses = do
  ([SomeSymFn sym]
lia_inv_fns, [BoolExpr t]
lia_horn_clauses, Map (SomeSymFn sym) (SomeSymFn sym)
_bv_to_lia_fn_subst) <- sym
-> Bool
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO
     ([SomeSymFn sym], [BoolExpr t],
      Map (SomeSymFn sym) (SomeSymFn sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Bool
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO
     ([SomeSymFn sym], [BoolExpr t],
      Map (SomeSymFn sym) (SomeSymFn sym))
transformHornClausesForZ3
    sym
sym
    Bool
do_bv_to_lia_transform
    [SomeSymFn sym]
inv_fns
    [BoolExpr t]
horn_clauses

  WriterConn t (Writer Z3)
writer <- Z3
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> IO (WriterConn t (Writer Z3))
forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> IO (WriterConn t (Writer a))
SMT2.defaultFileWriter
    Z3
Z3
    (Z3 -> String
forall a. Show a => a -> String
show Z3
Z3)
    (Z3 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures Z3
Z3)
    (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)
    sym
ExprBuilder t st fs
sym
    Handle
h
  WriterConn t (Writer Z3) -> IO ()
forall t. WriterConn t (Writer Z3) -> IO ()
forall a t.
SMTLib2GenericSolver a =>
WriterConn t (Writer a) -> IO ()
SMT2.setDefaultLogicAndOptions WriterConn t (Writer Z3)
writer
  sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeHornProblem sym
sym WriterConn t (Writer Z3)
writer [SomeSymFn sym]
lia_inv_fns [BoolExpr t]
lia_horn_clauses
  WriterConn t (Writer Z3) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeExit WriterConn t (Writer Z3)
writer

transformHornClausesForZ3 ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  Bool ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ([SomeSymFn sym], [BoolExpr t], Map (SomeSymFn sym) (SomeSymFn sym))
transformHornClausesForZ3 :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Bool
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO
     ([SomeSymFn sym], [BoolExpr t],
      Map (SomeSymFn sym) (SomeSymFn sym))
transformHornClausesForZ3 sym
sym Bool
do_bv_to_lia_transform [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses =
  if Bool
do_bv_to_lia_transform then do
    ([BoolExpr t]
lia_horn_clauses, Map (SomeSymFn sym) (SomeSymFn sym)
bv_to_lia_fn_subst) <- sym
-> [Pred sym]
-> IO ([Pred sym], Map (SomeSymFn sym) (SomeSymFn sym))
forall sym.
IsSymExprBuilder sym =>
sym
-> [Pred sym]
-> IO ([Pred sym], Map (SomeSymFn sym) (SomeSymFn sym))
transformPredBV2LIA sym
sym [Pred sym]
[BoolExpr t]
horn_clauses
    let lia_inv_fns :: [SomeSymFn sym]
lia_inv_fns = Map (SomeSymFn sym) (SomeSymFn sym) -> [SomeSymFn sym]
forall k a. Map k a -> [a]
Map.elems Map (SomeSymFn sym) (SomeSymFn sym)
bv_to_lia_fn_subst
    ([SomeSymFn sym], [BoolExpr t],
 Map (SomeSymFn sym) (SomeSymFn sym))
-> IO
     ([SomeSymFn sym], [BoolExpr t],
      Map (SomeSymFn sym) (SomeSymFn sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([SomeSymFn sym]
lia_inv_fns, [BoolExpr t]
lia_horn_clauses, Map (SomeSymFn sym) (SomeSymFn sym)
bv_to_lia_fn_subst)
  else ([SomeSymFn sym], [BoolExpr t],
 Map (SomeSymFn sym) (SomeSymFn sym))
-> IO
     ([SomeSymFn sym], [BoolExpr t],
      Map (SomeSymFn sym) (SomeSymFn sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([SomeSymFn sym]
inv_fns, [BoolExpr t]
horn_clauses, Map (SomeSymFn sym) (SomeSymFn sym)
forall k a. Map k a
Map.empty)

writeHornProblem ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  WriterConn t (SMT2.Writer Z3) ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ()
writeHornProblem :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeHornProblem sym
sym WriterConn t (Writer Z3)
writer [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses = do
  WriterConn t (Writer Z3) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer Z3)
writer Logic
Syntax.hornLogic
  [BoolExpr t]
implications <- (BoolExpr t -> IO (BoolExpr t)) -> [BoolExpr t] -> IO [BoolExpr t]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM
    (\BoolExpr t
clause -> (Some (ExprBoundVar t) -> BoolExpr t -> IO (BoolExpr t))
-> BoolExpr t -> Set (Some (ExprBoundVar t)) -> IO (BoolExpr t)
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM ((forall (tp :: BaseType).
 ExprBoundVar t tp -> BoolExpr t -> IO (BoolExpr t))
-> Some (ExprBoundVar t) -> BoolExpr t -> IO (BoolExpr t)
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome ((forall (tp :: BaseType).
  ExprBoundVar t tp -> BoolExpr t -> IO (BoolExpr t))
 -> Some (ExprBoundVar t) -> BoolExpr t -> IO (BoolExpr t))
-> (forall (tp :: BaseType).
    ExprBoundVar t tp -> BoolExpr t -> IO (BoolExpr t))
-> Some (ExprBoundVar t)
-> BoolExpr t
-> IO (BoolExpr t)
forall a b. (a -> b) -> a -> b
$ sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
forall (tp :: BaseType).
sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
forallPred sym
sym) BoolExpr t
clause (Set (Some (ExprBoundVar t)) -> IO (BoolExpr t))
-> Set (Some (ExprBoundVar t)) -> IO (BoolExpr t)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym -> Set (Some (BoundVar sym))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
forall (tp :: BaseType).
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
exprUninterpConstants sym
sym Pred sym
BoolExpr t
clause)
    [BoolExpr t]
horn_clauses
  (BoolExpr t -> IO ()) -> [BoolExpr t] -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (WriterConn t (Writer Z3) -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer Z3)
writer) [BoolExpr t]
implications
  WriterConn t (Writer Z3) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer Z3)
writer
  Bimap (SomeExprSymFn t) Text
fn_name_bimap <- WriterConn t (Writer Z3)
-> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
forall t h.
WriterConn t h
-> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
cacheLookupFnNameBimap WriterConn t (Writer Z3)
writer ([SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text))
-> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
forall a b. (a -> b) -> a -> b
$ (SomeSymFn sym -> SomeExprSymFn t)
-> [SomeSymFn sym] -> [SomeExprSymFn t]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeSymFn SymFn sym args ret
fn) -> ExprSymFn t args ret -> SomeExprSymFn t
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SomeExprSymFn t
SomeExprSymFn SymFn sym args ret
ExprSymFn t args ret
fn) [SomeSymFn sym]
inv_fns
  WriterConn t (Writer Z3) -> [Term] -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> [Term] -> IO ()
SMT2.writeGetValue WriterConn t (Writer Z3)
writer ([Term] -> IO ()) -> [Term] -> IO ()
forall a b. (a -> b) -> a -> b
$ (Text -> Term) -> [Text] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Term
forall v. SupportTermOps v => Text -> v
fromText ([Text] -> [Term]) -> [Text] -> [Term]
forall a b. (a -> b) -> a -> b
$ Bimap (SomeExprSymFn t) Text -> [Text]
forall a b. Bimap a b -> [b]
Bimap.elems Bimap (SomeExprSymFn t) Text
fn_name_bimap