{-# OPTIONS --allow-exec #-}
{-# OPTIONS --guardedness #-}
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
let (scr , parseOutputs) = toSMTLIBWithOutputParser scr
let cvc4Cmd = record
{ name = "cvc4"
; args = "--lang=smt2" ∷ "--output-lang=smt2" ∷ "--produce-models" ∷ "-q" ∷ "-" ∷ []
; input = scr
}
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)