{-# OPTIONS --allow-exec #-}
{-# OPTIONS --guardedness #-}

--------------------------------------------------------------------------------
-- Schmitty the Solver
--
-- Defines the `cvc4` tactic, which runs an SMT-LIB script using CVC4, as well
-- as the `solveCVC4` tactic, which translates the goal term to an SMT-LIB
-- script and solves it using CVC4.
--------------------------------------------------------------------------------

open import SMT.Theory

module SMT.Backend.CVC4 (theory : Theory) {{solvable : Solvable theory}} where

open Solvable solvable

open import Data.List as List using (List; _∷_; [])
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.String as String using (String; _++_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Unit as Unit using ()
open import Function using (case_of_; const; _$_; _∘_)
open import Reflection as Rfl using (return; _>>=_; _>>_)
open import Reflection.External
open import SMT.Backend.Base
open import SMT.Script.Base theory public

private
  variable
    Γ : Ctxt
    ξ : OutputType
    Ξ : OutputCtxt

cvc4TC : Script [] Γ (ξ  Ξ)  Rfl.TC (Outputs (ξ  Ξ))
cvc4TC {Γ} {ξ} {Ξ} scr = do

  -- Print the SMT-LIB script and build the output parser.
  let (scr , parseOutputs) = toSMTLIBWithOutputParser scr

  -- Construct the command specification.
  --
  -- TODO: Inspect the output type to see if any models should be produced,
  --       and set the --produce-models flag accordingly.
  --
  let cvc4Cmd = record
                { name  = "cvc4"
                ; args  = "--lang=smt2"  "--output-lang=smt2"  "--produce-models"  "-q"  "-"  []
                ; input = scr
                }

  -- Run the CVC4 command and parse the output.
  result exitCode stdout stderr  unsafeRunCmdTC cvc4Cmd
  case parseOutputs stdout of λ where
    (inj₁ smterr)  displayError stdout smterr (showCmdSpec cvc4Cmd) scr
    (inj₂ outputs)  return outputs

macro
  cvc4 : Script [] Γ (ξ  Ξ)  Rfl.Term  Rfl.TC 
  cvc4 scr hole = cvc4TC scr >>= Rfl.unify hole  quoteOutputs

macro
  solveCVC4 : {{Reflectable theory}}  Rfl.Term  Rfl.TC 
  solveCVC4 = solve "cvc4" cvc4TC
    where
      open Solver theory using (solve)