-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Control
  Copyright : ( c )  
-- License   : BSD3
-- Maintainer: 
-- Stability : experimental
--
  Control sublanguage for interacting with SMT solvers .
-----------------------------------------------------------------------------

{-# LANGUAGE ConstraintKinds #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Control (
     -- $queryIntro

     -- * User queries
       ExtractIO(..), MonadQuery(..), Queriable(..), Fresh(..), Query, query

     -- * Create a fresh variable
     , freshVar_, freshVar

     -- * Create a fresh array
     , freshArray_, freshArray

     -- * Checking satisfiability
     , CheckSatResult(..), checkSat, ensureSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet

     -- * Querying the solver
     -- ** Extracting values
     , getValue, registerUISMTFunction, getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables

     -- ** Extracting the unsat core
     , getUnsatCore

     -- ** Extracting a proof
     , getProof

     -- ** Extracting interpolants
     , getInterpolantMathSAT, getInterpolantZ3

     -- ** Extracting assertions
     , getAssertions

     -- * Getting solver information
     , SMTInfoFlag(..), SMTErrorBehavior(..), SMTInfoResponse(..)
     , getInfo, getOption

     -- * Entering and exiting assertion stack
     , getAssertionStackDepth, push, pop, inNewAssertionStack

     -- * Higher level tactics
     , caseSplit

     -- * Resetting the solver state
     , resetAssertions

     -- * Constructing assignments
     , (|->)

     -- * Terminating the query
     , mkSMTResult
     , exit

     -- * Controlling the solver behavior
     , ignoreExitCode, timeout

     -- * Miscellaneous
     , queryDebug
     , echo
     , io

     -- * Solver options
     , SMTOption(..)
     ) where

import Data.SBV.Core.Symbolic (MonadQuery(..), Query, Queriable(..), Fresh(..), Symbolic, QueryContext(..))

import Data.SBV.Control.BaseIO
import Data.SBV.Control.Query hiding (  getInfo, getOption, getUnknownReason, getObservables
                                      , getSMTResult, getLexicographicOptResults
                                      , getIndependentOptResults
                                      , getParetoOptResults, getModel
                                      , checkSatAssuming
                                      , checkSatAssumingWithUnsatisfiableSet
                                      , getAssertionStackDepth
                                      , inNewAssertionStack, push, pop
                                      , caseSplit, resetAssertions, echo, exit
                                      , getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3
                                      , getAssertions, getAssignment
                                      , mkSMTResult, freshVar_, freshVar
                                      , freshArray, freshArray_, checkSat, ensureSat
                                      , checkSatUsing, getValue
                                      , getUninterpretedValue, timeout, io)
import Data.SBV.Control.Utils (registerUISMTFunction)

import Data.SBV.Utils.ExtractIO (ExtractIO(..))

import qualified Data.SBV.Control.Utils as Trans

-- | Run a custom query
query :: Query a -> Symbolic a
query = Trans.executeQuery QueryExternal

  $ queryIntro 
 In certain cases , the user might want to take over the communication with the solver , programmatically 
 querying the engine and issuing commands accordingly . Queries can be extremely powerful as 
 they allow direct control of the solver . Here 's a simple example : 

 @ 
     module Test where 

     import Data . SBV 
     import Data . SBV.Control   -- queries require this module to be imported ! 

     test : : Symbolic ( Maybe ( Integer , Integer ) ) 
     test = do x < - sInteger " x "    -- a free variable named " x " 
               y < - sInteger " y "    -- a free variable named " y " 

               -- require the sum to be 10 
               constrain $ x + y .== 10 

               -- Go into the Query mode 
               query $ do 
                     -- Query the solver : Are the constraints satisfiable ? 
                     cs < - checkSat 
                     case cs of 
                       Unk     - > error " Solver said unknown ! " 
                       DSat { } - > error " Solver said DSat ! " 
                           return Nothing -- no solution ! 
                       Sat     - > -- Query the values : 
                                 do     x 
                                        y 

                                    io $ putStrLn $ " Solver returned : " + + show ( xv , yv ) 

                                    -- We can now add new constraints , 
                                    -- Or perform arbitrary computations and tell 
                                    -- the solver anything we want ! 
                                    constrain $ x . > literal xv + literal yv 

                                    -- call checkSat again 
                                    csNew < - checkSat 
                                    case csNew of 
                                      Unk     - > error " Solver said unknown ! " 
                                      DSat { } - > error " Solver said DSat ! " 
                                         > return Nothing 
                                      Sat     - > do xv2 < - getValue x 
                                                   yv2 < - getValue y 

                                                   return $ Just ( xv2 , yv2 ) 
 @ 

 Note the type of @test@ : it returns an optional pair of integers in the ' Symbolic ' monad . We turn 
 it into an IO value with the ' Data . SBV.Control.runSMT ' function : ( There 's also ' Data . SBV.Control.runSMTWith ' that uses a user specified 
 solver instead of the default . Note that ' Data . SBV.Provers.z3 ' is best supported ( and tested ) , if you use another solver your results may vary ! ) 

 @ 
     pair : : IO ( Maybe ( Integer , Integer ) ) 
     pair = runSMT test 
 @ 

 When run , this can return : 

 @ 
 * Test > pair 
 Solver returned : ( 10,0 ) 
 Just ( 11,-1 ) 
 @ 

 demonstrating that the user has full contact with the solver and can guide it as the program executes . SBV 
 provides access to many SMTLib features in the query mode , as exported from this very module . 

 For other examples see : 

   - " Documentation . SBV.Examples . Queries . AllSat " : Simulating SBV 's ' Data . SBV.allSat ' using queries . 
   - " Documentation . SBV.Examples . Queries .  " : Performing a case - split during a query . 
   - " Documentation . SBV.Examples . Queries . Enums " : Using enumerations in queries . 
   - " Documentation . SBV.Examples . Queries . FourFours " : Solution to a fun arithmetic puzzle , coded using queries . 
   - " Documentation . SBV.Examples . Queries . GuessNumber " : The famous number guessing game . 
   - " Documentation . SBV.Examples . Queries . UnsatCore " : Extracting unsat - cores using queries . 
   - " Documentation . SBV.Examples . Queries .  " : Extracting interpolants using queries . 

In certain cases, the user might want to take over the communication with the solver, programmatically
querying the engine and issuing commands accordingly. Queries can be extremely powerful as
they allow direct control of the solver. Here's a simple example:

@
    module Test where

    import Data.SBV
    import Data.SBV.Control  -- queries require this module to be imported!

    test :: Symbolic (Maybe (Integer, Integer))
    test = do x <- sInteger "x"   -- a free variable named "x"
              y <- sInteger "y"   -- a free variable named "y"

              -- require the sum to be 10
              constrain $ x + y .== 10

              -- Go into the Query mode
              query $ do
                    -- Query the solver: Are the constraints satisfiable?
                    cs <- checkSat
                    case cs of
                      Unk    -> error "Solver said unknown!"
                      DSat{} -> error "Solver said DSat!"
                      Unsat  -> return Nothing -- no solution!
                      Sat    -> -- Query the values:
                                do xv <- getValue x
                                   yv <- getValue y

                                   io $ putStrLn $ "Solver returned: " ++ show (xv, yv)

                                   -- We can now add new constraints,
                                   -- Or perform arbitrary computations and tell
                                   -- the solver anything we want!
                                   constrain $ x .> literal xv + literal yv

                                   -- call checkSat again
                                   csNew <- checkSat
                                   case csNew of
                                     Unk    -> error "Solver said unknown!"
                                     DSat{} -> error "Solver said DSat!"
                                     Unsat  -> return Nothing
                                     Sat    -> do xv2 <- getValue x
                                                  yv2 <- getValue y

                                                  return $ Just (xv2, yv2)
@

Note the type of @test@: it returns an optional pair of integers in the 'Symbolic' monad. We turn
it into an IO value with the 'Data.SBV.Control.runSMT' function: (There's also 'Data.SBV.Control.runSMTWith' that uses a user specified
solver instead of the default. Note that 'Data.SBV.Provers.z3' is best supported (and tested), if you use another solver your results may vary!)

@
    pair :: IO (Maybe (Integer, Integer))
    pair = runSMT test
@

When run, this can return:

@
*Test> pair
Solver returned: (10,0)
Just (11,-1)
@

demonstrating that the user has full contact with the solver and can guide it as the program executes. SBV
provides access to many SMTLib features in the query mode, as exported from this very module.

For other examples see:

  - "Documentation.SBV.Examples.Queries.AllSat": Simulating SBV's 'Data.SBV.allSat' using queries.
  - "Documentation.SBV.Examples.Queries.CaseSplit": Performing a case-split during a query.
  - "Documentation.SBV.Examples.Queries.Enums": Using enumerations in queries.
  - "Documentation.SBV.Examples.Queries.FourFours": Solution to a fun arithmetic puzzle, coded using queries.
  - "Documentation.SBV.Examples.Queries.GuessNumber": The famous number guessing game.
  - "Documentation.SBV.Examples.Queries.UnsatCore": Extracting unsat-cores using queries.
  - "Documentation.SBV.Examples.Queries.Interpolants": Extracting interpolants using queries.
-}

---------------------------------------------------------------------------
 |
 Module    : Data.SBV.Control
 License   : BSD3
 Maintainer: 
 Stability : experimental

---------------------------------------------------------------------------
# LANGUAGE ConstraintKinds #
# OPTIONS_GHC -Wall -Werror #
 $queryIntro
 * User queries
 * Create a fresh variable
 * Create a fresh array
 * Checking satisfiability
 * Querying the solver
 ** Extracting values
 ** Extracting the unsat core
 ** Extracting a proof
 ** Extracting interpolants
 ** Extracting assertions
 * Getting solver information
 * Entering and exiting assertion stack
 * Higher level tactics
 * Resetting the solver state
 * Constructing assignments
 * Terminating the query
 * Controlling the solver behavior
 * Miscellaneous
 * Solver options
 | Run a custom query
 queries require this module to be imported ! 
 a free variable named " x " 
 a free variable named " y " 
 require the sum to be 10 
 Go into the Query mode 
 Query the solver : Are the constraints satisfiable ? 
 no solution ! 
 Query the values : 
 We can now add new constraints , 
 Or perform arbitrary computations and tell 
 the solver anything we want ! 
 call checkSat again 
 queries require this module to be imported!
 a free variable named "x"
 a free variable named "y"
 require the sum to be 10
 Go into the Query mode
 Query the solver: Are the constraints satisfiable?
 no solution!
 Query the values:
 We can now add new constraints,
 Or perform arbitrary computations and tell
 the solver anything we want!
 call checkSat again
  Copyright : ( c )  
  Control sublanguage for interacting with SMT solvers .



module Data.SBV.Control (

       ExtractIO(..), MonadQuery(..), Queriable(..), Fresh(..), Query, query

     , freshVar_, freshVar

     , freshArray_, freshArray

     , CheckSatResult(..), checkSat, ensureSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet

     , getValue, registerUISMTFunction, getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables

     , getUnsatCore

     , getProof

     , getInterpolantMathSAT, getInterpolantZ3

     , getAssertions

     , SMTInfoFlag(..), SMTErrorBehavior(..), SMTInfoResponse(..)
     , getInfo, getOption

     , getAssertionStackDepth, push, pop, inNewAssertionStack

     , caseSplit

     , resetAssertions

     , (|->)

     , mkSMTResult
     , exit

     , ignoreExitCode, timeout

     , queryDebug
     , echo
     , io

     , SMTOption(..)
     ) where

import Data.SBV.Core.Symbolic (MonadQuery(..), Query, Queriable(..), Fresh(..), Symbolic, QueryContext(..))

import Data.SBV.Control.BaseIO
import Data.SBV.Control.Query hiding (  getInfo, getOption, getUnknownReason, getObservables
                                      , getSMTResult, getLexicographicOptResults
                                      , getIndependentOptResults
                                      , getParetoOptResults, getModel
                                      , checkSatAssuming
                                      , checkSatAssumingWithUnsatisfiableSet
                                      , getAssertionStackDepth
                                      , inNewAssertionStack, push, pop
                                      , caseSplit, resetAssertions, echo, exit
                                      , getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3
                                      , getAssertions, getAssignment
                                      , mkSMTResult, freshVar_, freshVar
                                      , freshArray, freshArray_, checkSat, ensureSat
                                      , checkSatUsing, getValue
                                      , getUninterpretedValue, timeout, io)
import Data.SBV.Control.Utils (registerUISMTFunction)

import Data.SBV.Utils.ExtractIO (ExtractIO(..))

import qualified Data.SBV.Control.Utils as Trans

query :: Query a -> Symbolic a
query = Trans.executeQuery QueryExternal

  $ queryIntro 
 In certain cases , the user might want to take over the communication with the solver , programmatically 
 querying the engine and issuing commands accordingly . Queries can be extremely powerful as 
 they allow direct control of the solver . Here 's a simple example : 

 @ 
     module Test where 

     import Data . SBV 

     test : : Symbolic ( Maybe ( Integer , Integer ) ) 

               constrain $ x + y .== 10 

               query $ do 
                     cs < - checkSat 
                     case cs of 
                       Unk     - > error " Solver said unknown ! " 
                       DSat { } - > error " Solver said DSat ! " 
                                 do     x 
                                        y 

                                    io $ putStrLn $ " Solver returned : " + + show ( xv , yv ) 

                                    constrain $ x . > literal xv + literal yv 

                                    csNew < - checkSat 
                                    case csNew of 
                                      Unk     - > error " Solver said unknown ! " 
                                      DSat { } - > error " Solver said DSat ! " 
                                         > return Nothing 
                                      Sat     - > do xv2 < - getValue x 
                                                   yv2 < - getValue y 

                                                   return $ Just ( xv2 , yv2 ) 
 @ 

 Note the type of @test@ : it returns an optional pair of integers in the ' Symbolic ' monad . We turn 
 it into an IO value with the ' Data . SBV.Control.runSMT ' function : ( There 's also ' Data . SBV.Control.runSMTWith ' that uses a user specified 
 solver instead of the default . Note that ' Data . SBV.Provers.z3 ' is best supported ( and tested ) , if you use another solver your results may vary ! ) 

 @ 
     pair : : IO ( Maybe ( Integer , Integer ) ) 
     pair = runSMT test 
 @ 

 When run , this can return : 

 @ 
 * Test > pair 
 Solver returned : ( 10,0 ) 
 Just ( 11,-1 ) 
 @ 

 demonstrating that the user has full contact with the solver and can guide it as the program executes . SBV 
 provides access to many SMTLib features in the query mode , as exported from this very module . 

 For other examples see : 

   - " Documentation . SBV.Examples . Queries . AllSat " : Simulating SBV 's ' Data . SBV.allSat ' using queries . 
   - " Documentation . SBV.Examples . Queries .  " : Performing a case - split during a query . 
   - " Documentation . SBV.Examples . Queries . Enums " : Using enumerations in queries . 
   - " Documentation . SBV.Examples . Queries . FourFours " : Solution to a fun arithmetic puzzle , coded using queries . 
   - " Documentation . SBV.Examples . Queries . GuessNumber " : The famous number guessing game . 
   - " Documentation . SBV.Examples . Queries . UnsatCore " : Extracting unsat - cores using queries . 
   - " Documentation . SBV.Examples . Queries .  " : Extracting interpolants using queries . 

In certain cases, the user might want to take over the communication with the solver, programmatically
querying the engine and issuing commands accordingly. Queries can be extremely powerful as
they allow direct control of the solver. Here's a simple example:

@
    module Test where

    import Data.SBV

    test :: Symbolic (Maybe (Integer, Integer))

              constrain $ x + y .== 10

              query $ do
                    cs <- checkSat
                    case cs of
                      Unk    -> error "Solver said unknown!"
                      DSat{} -> error "Solver said DSat!"
                                do xv <- getValue x
                                   yv <- getValue y

                                   io $ putStrLn $ "Solver returned: " ++ show (xv, yv)

                                   constrain $ x .> literal xv + literal yv

                                   csNew <- checkSat
                                   case csNew of
                                     Unk    -> error "Solver said unknown!"
                                     DSat{} -> error "Solver said DSat!"
                                     Unsat  -> return Nothing
                                     Sat    -> do xv2 <- getValue x
                                                  yv2 <- getValue y

                                                  return $ Just (xv2, yv2)
@

Note the type of @test@: it returns an optional pair of integers in the 'Symbolic' monad. We turn
it into an IO value with the 'Data.SBV.Control.runSMT' function: (There's also 'Data.SBV.Control.runSMTWith' that uses a user specified
solver instead of the default. Note that 'Data.SBV.Provers.z3' is best supported (and tested), if you use another solver your results may vary!)

@
    pair :: IO (Maybe (Integer, Integer))
    pair = runSMT test
@

When run, this can return:

@
*Test> pair
Solver returned: (10,0)
Just (11,-1)
@

demonstrating that the user has full contact with the solver and can guide it as the program executes. SBV
provides access to many SMTLib features in the query mode, as exported from this very module.

For other examples see:

  - "Documentation.SBV.Examples.Queries.AllSat": Simulating SBV's 'Data.SBV.allSat' using queries.
  - "Documentation.SBV.Examples.Queries.CaseSplit": Performing a case-split during a query.
  - "Documentation.SBV.Examples.Queries.Enums": Using enumerations in queries.
  - "Documentation.SBV.Examples.Queries.FourFours": Solution to a fun arithmetic puzzle, coded using queries.
  - "Documentation.SBV.Examples.Queries.GuessNumber": The famous number guessing game.
  - "Documentation.SBV.Examples.Queries.UnsatCore": Extracting unsat-cores using queries.
  - "Documentation.SBV.Examples.Queries.Interpolants": Extracting interpolants using queries.
-}
