-----------------------------------------------------------------------
-- |
-- Module           : What4.Concretize
-- Description      : Concretize values
-- Copyright        : (c) Galois, Inc 2024
-- License          : BSD3
-- Maintainer       : Langston Barrett <langston@galois.com>
-- Stability        : provisional
--
-- In our terminology, concretization is the process of (1) obtaining a
-- model from an SMT solver and (2) requesting the value of a particular set
-- of symbolic expressions in said model. The operation (2) alone is called
-- "grounding", see "What4.GroundEval".
-----------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

module What4.Concretize
  ( ConcretizationFailure(..)
  , concretize
  , UniqueConcretizationFailure(..)
  , uniquelyConcretize
  ) where

import qualified What4.Expr.Builder as WEB
import qualified What4.Expr.GroundEval as WEG
import qualified What4.Interface as WI
import qualified What4.Protocol.Online as WPO
import qualified What4.Protocol.SMTWriter as WPS
import qualified What4.SatResult as WSat

-- | Reasons why attempting to resolve a symbolic expression as ground can fail.
data ConcretizationFailure
  = SolverUnknown
    -- ^ Querying the SMT solver yielded @UNKNOWN@.
  | UnsatInitialAssumptions
    -- ^ Querying the SMT solver for an initial model of the expression failed
    -- due to the initial assumptions in scope being unsatisfiable.
  deriving Show

-- | Get a 'WEG.GroundValue' for a 'WI.SymExpr' by asking an online solver for
-- a model.
--
-- In contrast with 'uniquelyConcretize', this function returns the value of the
-- 'WI.SymExpr' in just one of potentially many distinct models. See the Haddock
-- on 'uniquelyConcretize' for a further comparison.
concretize ::
  ( sym ~ WEB.ExprBuilder scope st fs
  , WPO.OnlineSolver solver
  ) =>
  WPO.SolverProcess scope solver ->
  -- | The symbolic term to query from the model
  WI.SymExpr sym tp ->
  IO (Either ConcretizationFailure (WEG.GroundValue tp))
concretize sp val =
  case WEG.asGround val of
    Just gVal -> pure (Right gVal)
    Nothing -> do
      WPO.inNewFrame sp $ do
        msat <- WPO.checkAndGetModel sp "Ground value using model"
        case msat of
          WSat.Unknown -> pure $ Left SolverUnknown
          WSat.Unsat {} -> pure $ Left UnsatInitialAssumptions
          WSat.Sat mdl -> Right <$> WEG.groundEval mdl val

data UniqueConcretizationFailure
  = GroundingFailure ConcretizationFailure
  | MultipleModels
    -- ^ There are multiple possible models for the expression, which means it
    -- is truly symbolic and therefore unable to be uniquely concretized.
  deriving Show

-- | Attempt to resolve the given 'WI.SymExpr' to a unique concrete value using
-- an online SMT solver connection.
--
-- The implementation of this function (1) asks for a model from the solver.
-- If it gets one, it (2) adds a blocking clause and asks for another. If there
-- was only one model, concretize the initial value and return it with 'Right'.
-- Otherwise, return an explanation of why concretization failed with 'Left'.
-- This behavior is contrasted with 'concretize', which just does (1).
uniquelyConcretize ::
  ( sym ~ WEB.ExprBuilder scope st fs
  , WPO.OnlineSolver solver
  ) =>
  -- | The symbolic backend
  sym ->
  WPO.SolverProcess scope solver ->
  -- | The symbolic term to concretize
  WI.SymExpr sym tp ->
  IO (Either UniqueConcretizationFailure (WEG.GroundValue tp))
uniquelyConcretize sym sp val =
  case WEG.asGround val of
    Just gVal -> pure (Right gVal)
    Nothing -> do
      -- First, check to see if there is a model of the symbolic value.
      concVal_ <- concretize sp val
      case concVal_ of
        Left e -> pure (Left (GroundingFailure e))
        Right concVal -> do
          -- We found a model, so check to see if this is the only possible
          -- model for this symbolic value.  We do this by adding a blocking
          -- clause that assumes the `SymExpr` is /not/ equal to the model we
          -- found in the previous step. If this is unsatisfiable, the SymExpr
          -- can only be equal to that model, so we can conclude it is concrete.
          -- If it is satisfiable, on the other hand, the `SymExpr` can be
          -- multiple values, so it is truly symbolic.
          WPO.inNewFrame sp $ do
            injectedConcVal <- WEG.groundToSym sym (WI.exprType val) concVal
            eq <- WI.isEq sym val injectedConcVal
            block <- WI.notPred sym eq
            WPS.assume (WPO.solverConn sp) block
            msat' <- WPO.checkAndGetModel sp "Concretize value (with blocking clause)"
            case msat' of
              WSat.Unknown -> pure $ Left $ GroundingFailure $ SolverUnknown
              WSat.Sat _mdl -> pure $ Left $ MultipleModels
              WSat.Unsat {} -> pure $ Right concVal -- There is a single concrete result