{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}

module SMTLIB.Backends.Tests.Sources (Source (..), sources) where

import SMTLIB.Backends

-- | A source is a list of SMTLib2 commands, available in several different formats
-- for testing purposes.
data Source = Source
  { -- | The name of the source.
    Source -> String
name :: String,
    -- | A computation equivalent to sending the raw content of the source to the
    -- solver.
    Source -> Solver -> IO ()
run :: Solver -> IO ()
  }

-- | A list of examples SMT-LIB files. Most of them were taken from the official
-- SMT-LIB website:
-- https://smtlib.cs.uiowa.edu/examples.shtml
sources :: [Source]
sources =
  [ Source
assertions,
    Source
assignments,
    Source
boolean,
    Source
info,
    Source
integerArithmetic,
    Source
modelingSequentialCodeSSA,
    Source
modelingSequentialCodeBitvectors,
    Source
scopes,
    Source
sorts,
    Source
unsatCores,
    Source
valuesOrModels
  ]

assertions :: Source
assertions = String -> (Solver -> IO ()) -> Source
Source String
"assertions" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-option :produce-assertions true)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_UF)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const p Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const q Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(push 1)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (or p q))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(push 1)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (not q))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-assertions)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(pop 1)"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-assertions)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(pop 1)"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-assertions)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

assignments :: Source
assignments = String -> (Solver -> IO ()) -> Source
Source String
"assignments" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-option :produce-assignments true)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_UF)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const p Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const q Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const r Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (not (=(! (and (! p :named P) q) :named PQ) (! r :named R))))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-assignment)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

boolean :: Source
boolean = String -> (Solver -> IO ()) -> Source
Source String
"boolean" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_UF)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const p Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (and p (not p)))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

info :: Source
info = String -> (Solver -> IO ()) -> Source
Source String
"info" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-info :name)"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-info :version )"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-info :authors )"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

integerArithmetic :: Source
integerArithmetic = String -> (Solver -> IO ()) -> Source
Source String
"integer arithmetic" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_LIA)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const x Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const y Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (- x y) (+ x (- y) 1)))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

modelingSequentialCodeSSA :: Source
modelingSequentialCodeSSA = String -> (Solver -> IO ()) -> Source
Source String
"modeling sequential code (SSA)" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_UFLIA)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-option :produce-models true)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-fun x (Int) Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-fun y (Int) Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-fun t (Int) Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (t 0) (x 0)))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (y 1) (t 0)))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (x 1) (y 1)))"

  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (not (and (= (x 1) (y 0)) (= (y 1) (x 0)))))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-value ((x 0) (y 0) (x 1) (y 1)))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-model)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

modelingSequentialCodeBitvectors :: Source
modelingSequentialCodeBitvectors = String -> (Solver -> IO ()) -> Source
Source String
"modeling sequential code (bitvectors)" forall a b. (a -> b) -> a -> b
$
  \Solver
solver -> do
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_BV)"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-option :produce-models true)"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const x_0 (_ BitVec 32))"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const x_1 (_ BitVec 32))"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const x_2 (_ BitVec 32))"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const y_0 (_ BitVec 32))"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const y_1 (_ BitVec 32))"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= x_1 (bvadd x_0 y_0)))"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= y_1 (bvsub x_1 y_0)))"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= x_2 (bvsub x_1 y_1)))"
    Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (not (and (= x_2 y_0) (= y_1 x_0))))"
    ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
    forall (m :: * -> *) a. Monad m => a -> m a
return ()

scopes :: Source
scopes = String -> (Solver -> IO ()) -> Source
Source String
"scopes" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_LIA)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const x Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const y Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (+ x (* 2 y)) 20))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(push 1)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (- x y) 2))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(pop 1)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(push 1)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (- x y) 3))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(pop 1)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

sorts :: Source
sorts = String -> (Solver -> IO ()) -> Source
Source String
"sorts" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_UF)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-sort A 0)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const a A)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const b A)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const c A)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const d A)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const e A)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (or (= c a)(= c b)))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (or (= d a)(= d b)))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (or (= e a)(= e b)))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(push 1)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (distinct c d))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(pop 1)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(push 1)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (distinct c d e))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(pop 1)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

unsatCores :: Source
unsatCores = String -> (Solver -> IO ()) -> Source
Source String
"unsat cores" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-option :produce-unsat-cores true)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_UF)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const p Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const q Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const r Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const s Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const t Bool)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (! (=> p q) :named PQ))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (! (=> q r) :named QR))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (! (=> r s) :named RS))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (! (=> s t) :named ST))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (! (not (=> q s)) :named NQS))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-unsat-core)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

valuesOrModels :: Source
valuesOrModels = String -> (Solver -> IO ()) -> Source
Source String
"values or models" forall a b. (a -> b) -> a -> b
$ \Solver
solver -> do
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-option :produce-models true)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(set-logic QF_LIA)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const x Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(declare-const y Int)"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (+ x (* 2 y)) 20))"
  Solver -> Builder -> IO ()
command_ Solver
solver Builder
"(assert (= (- x y) 2))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(check-sat)"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-value (x y))"
  ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-model)"
  forall (m :: * -> *) a. Monad m => a -> m a
return ()