{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Backend.SBV.Data.SMT.Solving
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Backend.SBV.Data.SMT.Solving
  ( GrisetteSMTConfig (..),
    sbvConfig,
    TermTy,
  )
where

import Control.DeepSeq
import Control.Monad.Except
import qualified Data.HashSet as S
import Data.Hashable
import Data.Kind
import Data.List (partition)
import Data.Maybe
import qualified Data.SBV as SBV
import Data.SBV.Control (Query)
import qualified Data.SBV.Control as SBVC
import GHC.TypeNats
import Grisette.Backend.SBV.Data.SMT.Lowering
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.CEGISSolver
import Grisette.Core.Data.Class.Evaluate
import Grisette.Core.Data.Class.ExtractSymbolics
import Grisette.Core.Data.Class.GenSym
import Grisette.Core.Data.Class.ModelOps
import Grisette.Core.Data.Class.Solvable
import Grisette.Core.Data.Class.Solver
import Grisette.IR.SymPrim.Data.BV
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.Model as PM
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.SymPrim
import Grisette.IR.SymPrim.Data.TabularFun
import Language.Haskell.TH.Syntax (Lift)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.IR.SymPrim
-- >>> import Grisette.Backend.SBV

type Aux :: Bool -> Nat -> Type
type family Aux o n where
  Aux 'True n = SBV.SInteger
  Aux 'False n = SBV.SInt n

type IsZero :: Nat -> Bool
type family IsZero n where
  IsZero 0 = 'True
  IsZero _ = 'False

type TermTy :: Nat -> Type -> Type
type family TermTy bitWidth b where
  TermTy _ Bool = SBV.SBool
  TermTy n Integer = Aux (IsZero n) n
  TermTy n (IntN x) = SBV.SBV (SBV.IntN x)
  TermTy n (WordN x) = SBV.SBV (SBV.WordN x)
  TermTy n (a =-> b) = TermTy n a -> TermTy n b
  TermTy n (a --> b) = TermTy n a -> TermTy n b
  TermTy _ v = v

-- | Solver configuration for the Grisette SBV backend.
-- A Grisette solver configuration consists of a SBV solver configuration and
-- the reasoning precision.
--
-- Integers can be unbounded (mathematical integer) or bounded (machine
-- integer/bit vector). The two types of integers have their own use cases,
-- and should be used to model different systems.
-- However, the solvers are known to have bad performance on some unbounded
-- integer operations, for example, when reason about non-linear integer
-- algebraic (e.g., multiplication or division),
-- the solver may not be able to get a result in a reasonable time.
-- In contrast, reasoning about bounded integers is usually more efficient.
--
-- To bridge the performance gap between the two types of integers, Grisette
-- allows to model the system with unbounded integers, and evaluate them with
-- infinite precision during the symbolic evaluation, but when solving the
-- queries, they are translated to bit vectors for better performance.
--
-- For example, the Grisette term @5 * "a" :: SymInteger@ should be translated
-- to the following SMT with the unbounded reasoning configuration (the term
-- is @t1@):
--
-- > (declare-fun a () Int)           ; declare symbolic constant a
-- > (define-fun c1 () Int 5)         ; define the concrete value 5
-- > (define-fun t1 () Int (* c1 a))  ; define the term
--
-- While with reasoning precision 4, it would be translated to the following
-- SMT (the term is @t1@):
--
-- > ; declare symbolic constant a, the type is a bit vector with bit width 4
-- > (declare-fun a () (_ BitVec 4))
-- > ; define the concrete value 1, translated to the bit vector #x1
-- > (define-fun c1 () (_ BitVec 4) #x5)
-- > ; define the term, using bit vector addition rather than integer addition
-- > (define-fun t1 () (_ BitVec 4) (bvmul c1 a))
--
-- This bounded translation can usually be solved faster than the unbounded
-- one, and should work well when no overflow is possible, in which case the
-- performance can be improved with almost no cost.
--
-- We must note that the bounded translation is an approximation and is __/not/__
-- __/sound/__. As the approximation happens only during the final translation,
-- the symbolic evaluation may aggressively optimize the term based on the
-- properties of mathematical integer arithmetic. This may cause the solver yield
-- results that is incorrect under both unbounded or bounded semantics.
--
-- The following is an example that is correct under bounded semantics, while is
-- incorrect under the unbounded semantics:
--
-- >>> :set -XTypeApplications -XOverloadedStrings -XDataKinds
-- >>> let a = "a" :: SymInteger
-- >>> solve (UnboundedReasoning z3) $ a >~ 7 &&~ a <~ 9
-- Right (Model {a -> 8 :: Integer})
-- >>> solve (BoundedReasoning @4 z3) $ a >~ 7 &&~ a <~ 9
-- Left Unsat
--
-- This should be avoided by setting an large enough reasoning precision to prevent
-- overflows.
data GrisetteSMTConfig (integerBitWidth :: Nat) where
  UnboundedReasoning :: SBV.SMTConfig -> GrisetteSMTConfig 0
  BoundedReasoning ::
    (KnownNat integerBitWidth, IsZero integerBitWidth ~ 'False, SBV.BVIsNonZero integerBitWidth) =>
    SBV.SMTConfig ->
    GrisetteSMTConfig integerBitWidth

-- | Extract the SBV solver configuration from the Grisette solver configuration.
sbvConfig :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBV.SMTConfig
sbvConfig :: forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTConfig
sbvConfig (UnboundedReasoning SMTConfig
config) = SMTConfig
config
sbvConfig (BoundedReasoning SMTConfig
config) = SMTConfig
config

solveTermWith ::
  forall integerBitWidth.
  GrisetteSMTConfig integerBitWidth ->
  Term Bool ->
  IO (SymBiMap, Either SBVC.CheckSatResult PM.Model)
solveTermWith :: forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth
-> Term Bool -> IO (SymBiMap, Either CheckSatResult Model)
solveTermWith GrisetteSMTConfig integerBitWidth
config Term Bool
term = SMTConfig
-> Symbolic (SymBiMap, Either CheckSatResult Model)
-> IO (SymBiMap, Either CheckSatResult Model)
forall a. SMTConfig -> Symbolic a -> IO a
SBV.runSMTWith (GrisetteSMTConfig integerBitWidth -> SMTConfig
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTConfig
sbvConfig GrisetteSMTConfig integerBitWidth
config) (Symbolic (SymBiMap, Either CheckSatResult Model)
 -> IO (SymBiMap, Either CheckSatResult Model))
-> Symbolic (SymBiMap, Either CheckSatResult Model)
-> IO (SymBiMap, Either CheckSatResult Model)
forall a b. (a -> b) -> a -> b
$ do
  (SymBiMap
m, SBool
a) <- GrisetteSMTConfig integerBitWidth
-> Term Bool -> Symbolic (SymBiMap, TermTy integerBitWidth Bool)
forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim GrisetteSMTConfig integerBitWidth
config Term Bool
term
  Query (SymBiMap, Either CheckSatResult Model)
-> Symbolic (SymBiMap, Either CheckSatResult Model)
forall a. Query a -> Symbolic a
SBVC.query (Query (SymBiMap, Either CheckSatResult Model)
 -> Symbolic (SymBiMap, Either CheckSatResult Model))
-> Query (SymBiMap, Either CheckSatResult Model)
-> Symbolic (SymBiMap, Either CheckSatResult Model)
forall a b. (a -> b) -> a -> b
$ do
    SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain SBool
a
    CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
    case CheckSatResult
r of
      CheckSatResult
SBVC.Sat -> do
        SMTModel
md <- Query SMTModel
SBVC.getModel
        (SymBiMap, Either CheckSatResult Model)
-> Query (SymBiMap, Either CheckSatResult Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, Model -> Either CheckSatResult Model
forall a b. b -> Either a b
Right (Model -> Either CheckSatResult Model)
-> Model -> Either CheckSatResult Model
forall a b. (a -> b) -> a -> b
$ GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig integerBitWidth
config SMTModel
md SymBiMap
m)
      CheckSatResult
_ -> (SymBiMap, Either CheckSatResult Model)
-> Query (SymBiMap, Either CheckSatResult Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, CheckSatResult -> Either CheckSatResult Model
forall a b. a -> Either a b
Left CheckSatResult
r)

instance Solver (GrisetteSMTConfig n) SBVC.CheckSatResult where
  solve :: GrisetteSMTConfig n -> SymBool -> IO (Either CheckSatResult Model)
solve GrisetteSMTConfig n
config (Sym Term Bool
t) = (SymBiMap, Either CheckSatResult Model)
-> Either CheckSatResult Model
forall a b. (a, b) -> b
snd ((SymBiMap, Either CheckSatResult Model)
 -> Either CheckSatResult Model)
-> IO (SymBiMap, Either CheckSatResult Model)
-> IO (Either CheckSatResult Model)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GrisetteSMTConfig n
-> Term Bool -> IO (SymBiMap, Either CheckSatResult Model)
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth
-> Term Bool -> IO (SymBiMap, Either CheckSatResult Model)
solveTermWith GrisetteSMTConfig n
config Term Bool
t
  solveMulti :: GrisetteSMTConfig n -> Int -> SymBool -> IO [Model]
solveMulti GrisetteSMTConfig n
config Int
n s :: SymBool
s@(Sym Term Bool
t)
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = SMTConfig -> Symbolic [Model] -> IO [Model]
forall a. SMTConfig -> Symbolic a -> IO a
SBV.runSMTWith (GrisetteSMTConfig n -> SMTConfig
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTConfig
sbvConfig GrisetteSMTConfig n
config) (Symbolic [Model] -> IO [Model]) -> Symbolic [Model] -> IO [Model]
forall a b. (a -> b) -> a -> b
$ do
        (SymBiMap
newm, SBool
a) <- GrisetteSMTConfig n
-> Term Bool -> Symbolic (SymBiMap, TermTy n Bool)
forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim GrisetteSMTConfig n
config Term Bool
t
        Query [Model] -> Symbolic [Model]
forall a. Query a -> Symbolic a
SBVC.query (Query [Model] -> Symbolic [Model])
-> Query [Model] -> Symbolic [Model]
forall a b. (a -> b) -> a -> b
$ do
          SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain SBool
a
          CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
          case CheckSatResult
r of
            CheckSatResult
SBVC.Sat -> do
              SMTModel
md <- Query SMTModel
SBVC.getModel
              let model :: Model
model = GrisetteSMTConfig n -> SMTModel -> SymBiMap -> Model
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
md SymBiMap
newm
              Int -> Model -> SymBiMap -> Query [Model]
remainingModels Int
n Model
model SymBiMap
newm
            CheckSatResult
_ -> [Model] -> Query [Model]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    | Bool
otherwise = [Model] -> IO [Model]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    where
      allSymbols :: SymbolSet
allSymbols = SymBool -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics SymBool
s :: SymbolSet
      next :: PM.Model -> SymBiMap -> Query (SymBiMap, Either SBVC.CheckSatResult PM.Model)
      next :: Model -> SymBiMap -> Query (SymBiMap, Either CheckSatResult Model)
next Model
md SymBiMap
origm = do
        let newtm :: Term Bool
newtm =
              (Term Bool -> SomeTypedSymbol -> Term Bool)
-> Term Bool -> HashSet SomeTypedSymbol -> Term Bool
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl'
                (\Term Bool
acc (SomeTypedSymbol TypeRep t
_ TypedSymbol t
v) -> Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
acc (Term Bool -> Term Bool
pevalNotTerm (Maybe (Term Bool) -> Term Bool
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Term Bool) -> Term Bool) -> Maybe (Term Bool) -> Term Bool
forall a b. (a -> b) -> a -> b
$ TypedSymbol t -> Model -> Maybe (Term Bool)
forall a. TypedSymbol a -> Model -> Maybe (Term Bool)
equation TypedSymbol t
v Model
md)))
                (Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Bool
False)
                (SymbolSet -> HashSet SomeTypedSymbol
unSymbolSet SymbolSet
allSymbols)
        let (SBool
lowered, SymBiMap
newm) = GrisetteSMTConfig n
-> Term Bool -> SymBiMap -> (TermTy n Bool, SymBiMap)
forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> (TermTy integerBitWidth a, SymBiMap)
lowerSinglePrim' GrisetteSMTConfig n
config Term Bool
newtm SymBiMap
origm
        SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain SBool
lowered
        CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
        case CheckSatResult
r of
          CheckSatResult
SBVC.Sat -> do
            SMTModel
md1 <- Query SMTModel
SBVC.getModel
            let model :: Model
model = GrisetteSMTConfig n -> SMTModel -> SymBiMap -> Model
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
md1 SymBiMap
newm
            (SymBiMap, Either CheckSatResult Model)
-> Query (SymBiMap, Either CheckSatResult Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
newm, Model -> Either CheckSatResult Model
forall a b. b -> Either a b
Right Model
model)
          CheckSatResult
_ -> (SymBiMap, Either CheckSatResult Model)
-> Query (SymBiMap, Either CheckSatResult Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
newm, CheckSatResult -> Either CheckSatResult Model
forall a b. a -> Either a b
Left CheckSatResult
r)
      remainingModels :: Int -> PM.Model -> SymBiMap -> Query [PM.Model]
      remainingModels :: Int -> Model -> SymBiMap -> Query [Model]
remainingModels Int
n1 Model
md SymBiMap
origm
        | Int
n1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 = do
            (SymBiMap
newm, Either CheckSatResult Model
r) <- Model -> SymBiMap -> Query (SymBiMap, Either CheckSatResult Model)
next Model
md SymBiMap
origm
            case Either CheckSatResult Model
r of
              Left CheckSatResult
_ -> [Model] -> Query [Model]
forall (m :: * -> *) a. Monad m => a -> m a
return [Model
md]
              Right Model
mo -> do
                [Model]
rmmd <- Int -> Model -> SymBiMap -> Query [Model]
remainingModels (Int
n1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Model
mo SymBiMap
newm
                [Model] -> Query [Model]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Model] -> Query [Model]) -> [Model] -> Query [Model]
forall a b. (a -> b) -> a -> b
$ Model
md Model -> [Model] -> [Model]
forall a. a -> [a] -> [a]
: [Model]
rmmd
        | Bool
otherwise = [Model] -> Query [Model]
forall (m :: * -> *) a. Monad m => a -> m a
return [Model
md]
  solveAll :: GrisetteSMTConfig n -> SymBool -> IO [Model]
solveAll = GrisetteSMTConfig n -> SymBool -> IO [Model]
forall a. HasCallStack => a
undefined

instance CEGISSolver (GrisetteSMTConfig n) SBVC.CheckSatResult where
  cegisMultiInputs ::
    forall inputs spec.
    (ExtractSymbolics inputs, EvaluateSym inputs) =>
    GrisetteSMTConfig n ->
    [inputs] ->
    (inputs -> CEGISCondition) ->
    IO (Either SBVC.CheckSatResult ([inputs], PM.Model))
  cegisMultiInputs :: forall inputs spec.
(ExtractSymbolics inputs, EvaluateSym inputs) =>
GrisetteSMTConfig n
-> [inputs]
-> (inputs -> CEGISCondition)
-> IO (Either CheckSatResult ([inputs], Model))
cegisMultiInputs GrisetteSMTConfig n
config [inputs]
inputs inputs -> CEGISCondition
func =
    SymBool
-> [inputs]
-> Model
-> [inputs]
-> SymBool
-> SymBool
-> [inputs]
-> IO (Either CheckSatResult ([inputs], Model))
go1 ([inputs] -> SymBool
cexesAssertFun [inputs]
conInputs) [inputs]
conInputs ([Char] -> Model
forall a. HasCallStack => [Char] -> a
error [Char]
"Should have at least one gen") [] (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True) [inputs]
symInputs
    where
      ([inputs]
conInputs, [inputs]
symInputs) = (inputs -> Bool) -> [inputs] -> ([inputs], [inputs])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (SymbolSet -> Bool
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet -> Bool
isEmptySet (SymbolSet -> Bool) -> (inputs -> SymbolSet) -> inputs -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. inputs -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics) [inputs]
inputs
      go1 :: SymBool
-> [inputs]
-> Model
-> [inputs]
-> SymBool
-> SymBool
-> [inputs]
-> IO (Either CheckSatResult ([inputs], Model))
go1 SymBool
cexFormula [inputs]
cexes Model
previousModel [inputs]
inputs SymBool
pre SymBool
post [inputs]
remainingSymInputs = do
        case [inputs]
remainingSymInputs of
          [] -> Either CheckSatResult ([inputs], Model)
-> IO (Either CheckSatResult ([inputs], Model))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either CheckSatResult ([inputs], Model)
 -> IO (Either CheckSatResult ([inputs], Model)))
-> Either CheckSatResult ([inputs], Model)
-> IO (Either CheckSatResult ([inputs], Model))
forall a b. (a -> b) -> a -> b
$ ([inputs], Model) -> Either CheckSatResult ([inputs], Model)
forall a b. b -> Either a b
Right ([inputs]
cexes, Model
previousModel)
          inputs
newInput : [inputs]
vs -> do
            let CEGISCondition SymBool
nextPre SymBool
nextPost = inputs -> CEGISCondition
func inputs
newInput
            let finalPre :: SymBool
finalPre = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ SymBool
nextPre
            let finalPost :: SymBool
finalPost = SymBool
post SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ SymBool
nextPost
            Either CheckSatResult ([inputs], Model)
r <- SymBool
-> inputs
-> [inputs]
-> SymBool
-> SymBool
-> IO (Either CheckSatResult ([inputs], Model))
go SymBool
cexFormula inputs
newInput (inputs
newInput inputs -> [inputs] -> [inputs]
forall a. a -> [a] -> [a]
: [inputs]
inputs) SymBool
finalPre SymBool
finalPost
            case Either CheckSatResult ([inputs], Model)
r of
              Left CheckSatResult
failure -> Either CheckSatResult ([inputs], Model)
-> IO (Either CheckSatResult ([inputs], Model))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either CheckSatResult ([inputs], Model)
 -> IO (Either CheckSatResult ([inputs], Model)))
-> Either CheckSatResult ([inputs], Model)
-> IO (Either CheckSatResult ([inputs], Model))
forall a b. (a -> b) -> a -> b
$ CheckSatResult -> Either CheckSatResult ([inputs], Model)
forall a b. a -> Either a b
Left CheckSatResult
failure
              Right ([inputs]
newCexes, Model
mo) -> do
                SymBool
-> [inputs]
-> Model
-> [inputs]
-> SymBool
-> SymBool
-> [inputs]
-> IO (Either CheckSatResult ([inputs], Model))
go1
                  (SymBool
cexFormula SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ [inputs] -> SymBool
cexesAssertFun [inputs]
newCexes)
                  ([inputs]
cexes [inputs] -> [inputs] -> [inputs]
forall a. [a] -> [a] -> [a]
++ [inputs]
newCexes)
                  Model
mo
                  (inputs
newInput inputs -> [inputs] -> [inputs]
forall a. a -> [a] -> [a]
: [inputs]
inputs)
                  SymBool
finalPre
                  SymBool
finalPost
                  [inputs]
vs
      cexAssertFun :: inputs -> SymBool
cexAssertFun inputs
input =
        let CEGISCondition SymBool
pre SymBool
post = inputs -> CEGISCondition
func inputs
input in SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ SymBool
post
      cexesAssertFun :: [inputs] -> SymBool
      cexesAssertFun :: [inputs] -> SymBool
cexesAssertFun = (SymBool -> inputs -> SymBool) -> SymBool -> [inputs] -> SymBool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\SymBool
acc inputs
x -> SymBool
acc SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ inputs -> SymBool
cexAssertFun inputs
x) (Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True)
      go ::
        SymBool ->
        inputs ->
        [inputs] ->
        SymBool ->
        SymBool ->
        IO (Either SBVC.CheckSatResult ([inputs], PM.Model))
      go :: SymBool
-> inputs
-> [inputs]
-> SymBool
-> SymBool
-> IO (Either CheckSatResult ([inputs], Model))
go SymBool
cexFormula inputs
inputs [inputs]
allInputs SymBool
pre SymBool
post =
        SMTConfig
-> Symbolic (Either CheckSatResult ([inputs], Model))
-> IO (Either CheckSatResult ([inputs], Model))
forall a. SMTConfig -> Symbolic a -> IO a
SBV.runSMTWith (GrisetteSMTConfig n -> SMTConfig
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTConfig
sbvConfig GrisetteSMTConfig n
config) (Symbolic (Either CheckSatResult ([inputs], Model))
 -> IO (Either CheckSatResult ([inputs], Model)))
-> Symbolic (Either CheckSatResult ([inputs], Model))
-> IO (Either CheckSatResult ([inputs], Model))
forall a b. (a -> b) -> a -> b
$ do
          let Sym Term Bool
t = SymBool
phi SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ SymBool
cexFormula
          (SymBiMap
newm, SBool
a) <- GrisetteSMTConfig n
-> Term Bool -> Symbolic (SymBiMap, TermTy n Bool)
forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim GrisetteSMTConfig n
config Term Bool
t
          Query (Either CheckSatResult ([inputs], Model))
-> Symbolic (Either CheckSatResult ([inputs], Model))
forall a. Query a -> Symbolic a
SBVC.query (Query (Either CheckSatResult ([inputs], Model))
 -> Symbolic (Either CheckSatResult ([inputs], Model)))
-> Query (Either CheckSatResult ([inputs], Model))
-> Symbolic (Either CheckSatResult ([inputs], Model))
forall a b. (a -> b) -> a -> b
$
            (SymBiMap, Either CheckSatResult ([inputs], Model))
-> Either CheckSatResult ([inputs], Model)
forall a b. (a, b) -> b
snd ((SymBiMap, Either CheckSatResult ([inputs], Model))
 -> Either CheckSatResult ([inputs], Model))
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
-> Query (Either CheckSatResult ([inputs], Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain SBool
a
              CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
              Either CheckSatResult Model
mr <- case CheckSatResult
r of
                CheckSatResult
SBVC.Sat -> do
                  SMTModel
md <- Query SMTModel
SBVC.getModel
                  Either CheckSatResult Model
-> QueryT IO (Either CheckSatResult Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either CheckSatResult Model
 -> QueryT IO (Either CheckSatResult Model))
-> Either CheckSatResult Model
-> QueryT IO (Either CheckSatResult Model)
forall a b. (a -> b) -> a -> b
$ Model -> Either CheckSatResult Model
forall a b. b -> Either a b
Right (Model -> Either CheckSatResult Model)
-> Model -> Either CheckSatResult Model
forall a b. (a -> b) -> a -> b
$ GrisetteSMTConfig n -> SMTModel -> SymBiMap -> Model
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
md SymBiMap
newm
                CheckSatResult
_ -> Either CheckSatResult Model
-> QueryT IO (Either CheckSatResult Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either CheckSatResult Model
 -> QueryT IO (Either CheckSatResult Model))
-> Either CheckSatResult Model
-> QueryT IO (Either CheckSatResult Model)
forall a b. (a -> b) -> a -> b
$ CheckSatResult -> Either CheckSatResult Model
forall a b. a -> Either a b
Left CheckSatResult
r
              Either CheckSatResult Model
-> [inputs]
-> SymBiMap
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
loop ((SymbolSet
forallSymbols SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
`exceptFor`) (Model -> Model)
-> Either CheckSatResult Model -> Either CheckSatResult Model
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either CheckSatResult Model
mr) [] SymBiMap
newm
        where
          forallSymbols :: SymbolSet
          forallSymbols :: SymbolSet
forallSymbols = [inputs] -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics [inputs]
allInputs
          phi :: SymBool
phi = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ SymBool
post
          negphi :: SymBool
negphi = SymBool
pre SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ SymBool -> SymBool
forall b. LogicalOp b => b -> b
nots SymBool
post
          check :: Model -> IO (Either SBVC.CheckSatResult (inputs, PM.Model))
          check :: Model -> IO (Either CheckSatResult (inputs, Model))
check Model
candidate = do
            let evaluated :: SymBool
evaluated = Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
candidate SymBool
negphi
            Either CheckSatResult Model
r <- GrisetteSMTConfig n -> SymBool -> IO (Either CheckSatResult Model)
forall config failure.
Solver config failure =>
config -> SymBool -> IO (Either failure Model)
solve GrisetteSMTConfig n
config SymBool
evaluated
            Either CheckSatResult (inputs, Model)
-> IO (Either CheckSatResult (inputs, Model))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either CheckSatResult (inputs, Model)
 -> IO (Either CheckSatResult (inputs, Model)))
-> Either CheckSatResult (inputs, Model)
-> IO (Either CheckSatResult (inputs, Model))
forall a b. (a -> b) -> a -> b
$ do
              Model
m <- Either CheckSatResult Model
r
              let newm :: Model
newm = SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exact SymbolSet
forallSymbols Model
m
              (inputs, Model) -> Either CheckSatResult (inputs, Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Model -> inputs -> inputs
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
newm inputs
inputs, Model
newm)
          guess :: Model -> SymBiMap -> Query (SymBiMap, Either SBVC.CheckSatResult PM.Model)
          guess :: Model -> SymBiMap -> Query (SymBiMap, Either CheckSatResult Model)
guess Model
candidate SymBiMap
origm = do
            let Sym Term Bool
evaluated = Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
False Model
candidate SymBool
phi
            let (SBool
lowered, SymBiMap
newm) = GrisetteSMTConfig n
-> Term Bool -> SymBiMap -> (TermTy n Bool, SymBiMap)
forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> (TermTy integerBitWidth a, SymBiMap)
lowerSinglePrim' GrisetteSMTConfig n
config Term Bool
evaluated SymBiMap
origm
            SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
SBV.constrain SBool
lowered
            CheckSatResult
r <- Query CheckSatResult
SBVC.checkSat
            case CheckSatResult
r of
              CheckSatResult
SBVC.Sat -> do
                SMTModel
md <- Query SMTModel
SBVC.getModel
                let model :: Model
model = GrisetteSMTConfig n -> SMTModel -> SymBiMap -> Model
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
md SymBiMap
newm
                (SymBiMap, Either CheckSatResult Model)
-> Query (SymBiMap, Either CheckSatResult Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
newm, Model -> Either CheckSatResult Model
forall a b. b -> Either a b
Right (Model -> Either CheckSatResult Model)
-> Model -> Either CheckSatResult Model
forall a b. (a -> b) -> a -> b
$ SymbolSet -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
symbolSet -> model -> model
exceptFor SymbolSet
forallSymbols Model
model)
              CheckSatResult
_ -> (SymBiMap, Either CheckSatResult Model)
-> Query (SymBiMap, Either CheckSatResult Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
newm, CheckSatResult -> Either CheckSatResult Model
forall a b. a -> Either a b
Left CheckSatResult
r)
          loop ::
            Either SBVC.CheckSatResult PM.Model ->
            [inputs] ->
            SymBiMap ->
            Query (SymBiMap, Either SBVC.CheckSatResult ([inputs], PM.Model))
          loop :: Either CheckSatResult Model
-> [inputs]
-> SymBiMap
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
loop (Right Model
mo) [inputs]
cexs SymBiMap
origm = do
            Either CheckSatResult (inputs, Model)
r <- IO (Either CheckSatResult (inputs, Model))
-> QueryT IO (Either CheckSatResult (inputs, Model))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either CheckSatResult (inputs, Model))
 -> QueryT IO (Either CheckSatResult (inputs, Model)))
-> IO (Either CheckSatResult (inputs, Model))
-> QueryT IO (Either CheckSatResult (inputs, Model))
forall a b. (a -> b) -> a -> b
$ Model -> IO (Either CheckSatResult (inputs, Model))
check Model
mo
            case Either CheckSatResult (inputs, Model)
r of
              Left CheckSatResult
SBVC.Unsat -> (SymBiMap, Either CheckSatResult ([inputs], Model))
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
origm, ([inputs], Model) -> Either CheckSatResult ([inputs], Model)
forall a b. b -> Either a b
Right ([inputs]
cexs, Model
mo))
              Left CheckSatResult
v -> (SymBiMap, Either CheckSatResult ([inputs], Model))
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
origm, CheckSatResult -> Either CheckSatResult ([inputs], Model)
forall a b. a -> Either a b
Left CheckSatResult
v)
              Right (inputs
cex, Model
cexm) -> do
                (SymBiMap
newm, Either CheckSatResult Model
res) <- Model -> SymBiMap -> Query (SymBiMap, Either CheckSatResult Model)
guess Model
cexm SymBiMap
origm
                Either CheckSatResult Model
-> [inputs]
-> SymBiMap
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
loop Either CheckSatResult Model
res (inputs
cex inputs -> [inputs] -> [inputs]
forall a. a -> [a] -> [a]
: [inputs]
cexs) SymBiMap
newm
          loop (Left CheckSatResult
v) [inputs]
_ SymBiMap
origm = (SymBiMap, Either CheckSatResult ([inputs], Model))
-> QueryT IO (SymBiMap, Either CheckSatResult ([inputs], Model))
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
origm, CheckSatResult -> Either CheckSatResult ([inputs], Model)
forall a b. a -> Either a b
Left CheckSatResult
v)

newtype CegisInternal = CegisInternal Int
  deriving (CegisInternal -> CegisInternal -> Bool
(CegisInternal -> CegisInternal -> Bool)
-> (CegisInternal -> CegisInternal -> Bool) -> Eq CegisInternal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CegisInternal -> CegisInternal -> Bool
$c/= :: CegisInternal -> CegisInternal -> Bool
== :: CegisInternal -> CegisInternal -> Bool
$c== :: CegisInternal -> CegisInternal -> Bool
Eq, Int -> CegisInternal -> ShowS
[CegisInternal] -> ShowS
CegisInternal -> [Char]
(Int -> CegisInternal -> ShowS)
-> (CegisInternal -> [Char])
-> ([CegisInternal] -> ShowS)
-> Show CegisInternal
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CegisInternal] -> ShowS
$cshowList :: [CegisInternal] -> ShowS
show :: CegisInternal -> [Char]
$cshow :: CegisInternal -> [Char]
showsPrec :: Int -> CegisInternal -> ShowS
$cshowsPrec :: Int -> CegisInternal -> ShowS
Show, Eq CegisInternal
Eq CegisInternal
-> (CegisInternal -> CegisInternal -> Ordering)
-> (CegisInternal -> CegisInternal -> Bool)
-> (CegisInternal -> CegisInternal -> Bool)
-> (CegisInternal -> CegisInternal -> Bool)
-> (CegisInternal -> CegisInternal -> Bool)
-> (CegisInternal -> CegisInternal -> CegisInternal)
-> (CegisInternal -> CegisInternal -> CegisInternal)
-> Ord CegisInternal
CegisInternal -> CegisInternal -> Bool
CegisInternal -> CegisInternal -> Ordering
CegisInternal -> CegisInternal -> CegisInternal
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CegisInternal -> CegisInternal -> CegisInternal
$cmin :: CegisInternal -> CegisInternal -> CegisInternal
max :: CegisInternal -> CegisInternal -> CegisInternal
$cmax :: CegisInternal -> CegisInternal -> CegisInternal
>= :: CegisInternal -> CegisInternal -> Bool
$c>= :: CegisInternal -> CegisInternal -> Bool
> :: CegisInternal -> CegisInternal -> Bool
$c> :: CegisInternal -> CegisInternal -> Bool
<= :: CegisInternal -> CegisInternal -> Bool
$c<= :: CegisInternal -> CegisInternal -> Bool
< :: CegisInternal -> CegisInternal -> Bool
$c< :: CegisInternal -> CegisInternal -> Bool
compare :: CegisInternal -> CegisInternal -> Ordering
$ccompare :: CegisInternal -> CegisInternal -> Ordering
Ord, (forall (m :: * -> *). Quote m => CegisInternal -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    CegisInternal -> Code m CegisInternal)
-> Lift CegisInternal
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => CegisInternal -> m Exp
forall (m :: * -> *).
Quote m =>
CegisInternal -> Code m CegisInternal
liftTyped :: forall (m :: * -> *).
Quote m =>
CegisInternal -> Code m CegisInternal
$cliftTyped :: forall (m :: * -> *).
Quote m =>
CegisInternal -> Code m CegisInternal
lift :: forall (m :: * -> *). Quote m => CegisInternal -> m Exp
$clift :: forall (m :: * -> *). Quote m => CegisInternal -> m Exp
Lift)
  deriving newtype (Int -> CegisInternal -> Int
CegisInternal -> Int
(Int -> CegisInternal -> Int)
-> (CegisInternal -> Int) -> Hashable CegisInternal
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: CegisInternal -> Int
$chash :: CegisInternal -> Int
hashWithSalt :: Int -> CegisInternal -> Int
$chashWithSalt :: Int -> CegisInternal -> Int
Hashable, CegisInternal -> ()
(CegisInternal -> ()) -> NFData CegisInternal
forall a. (a -> ()) -> NFData a
rnf :: CegisInternal -> ()
$crnf :: CegisInternal -> ()
NFData)