{-# 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.
    name :: String,
    -- | A computation equivalent to sending the raw content of the source to the
    -- solver.
    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 =
  [ assertions,
    assignments,
    boolean,
    info,
    integerArithmetic,
    modelingSequentialCodeSSA,
    modelingSequentialCodeBitvectors,
    scopes,
    sorts,
    unsatCores,
    valuesOrModels
  ]

assertions = Source "assertions" $ \solver -> do
  command_ solver "(set-option :produce-assertions true)"
  command_ solver "(set-logic QF_UF)"
  command_ solver "(declare-const p Bool)"
  command_ solver "(declare-const q Bool)"
  command_ solver "(push 1)"
  command_ solver "(assert (or p q))"
  command_ solver "(push 1)"
  command_ solver "(assert (not q))"
  _ <- command solver "(get-assertions)"
  command_ solver "(pop 1)"
  _ <- command solver "(get-assertions)"
  command_ solver "(pop 1)"
  _ <- command solver "(get-assertions)"
  return ()

assignments = Source "assignments" $ \solver -> do
  command_ solver "(set-option :produce-assignments true)"
  command_ solver "(set-logic QF_UF)"
  command_ solver "(declare-const p Bool)"
  command_ solver "(declare-const q Bool)"
  command_ solver "(declare-const r Bool)"
  command_ solver "(assert (not (=(! (and (! p :named P) q) :named PQ) (! r :named R))))"
  _ <- command solver "(check-sat)"
  _ <- command solver "(get-assignment)"
  return ()

boolean = Source "boolean" $ \solver -> do
  command_ solver "(set-logic QF_UF)"
  command_ solver "(declare-const p Bool)"
  command_ solver "(assert (and p (not p)))"
  _ <- command solver "(check-sat)"
  return ()

info = Source "info" $ \solver -> do
  _ <- command solver "(get-info :name)"
  _ <- command solver "(get-info :version )"
  _ <- command solver "(get-info :authors )"
  return ()

integerArithmetic = Source "integer arithmetic" $ \solver -> do
  command_ solver "(set-logic QF_LIA)"
  command_ solver "(declare-const x Int)"
  command_ solver "(declare-const y Int)"
  command_ solver "(assert (= (- x y) (+ x (- y) 1)))"
  _ <- command solver "(check-sat)"
  return ()

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

  command_ solver "(assert (not (and (= (x 1) (y 0)) (= (y 1) (x 0)))))"
  _ <- command solver "(check-sat)"
  _ <- command solver "(get-value ((x 0) (y 0) (x 1) (y 1)))"
  _ <- command solver "(get-model)"
  return ()

modelingSequentialCodeBitvectors = Source "modeling sequential code (bitvectors)" $
  \solver -> do
    command_ solver "(set-logic QF_BV)"
    command_ solver "(set-option :produce-models true)"
    command_ solver "(declare-const x_0 (_ BitVec 32))"
    command_ solver "(declare-const x_1 (_ BitVec 32))"
    command_ solver "(declare-const x_2 (_ BitVec 32))"
    command_ solver "(declare-const y_0 (_ BitVec 32))"
    command_ solver "(declare-const y_1 (_ BitVec 32))"
    command_ solver "(assert (= x_1 (bvadd x_0 y_0)))"
    command_ solver "(assert (= y_1 (bvsub x_1 y_0)))"
    command_ solver "(assert (= x_2 (bvsub x_1 y_1)))"
    command_ solver "(assert (not (and (= x_2 y_0) (= y_1 x_0))))"
    _ <- command solver "(check-sat)"
    return ()

scopes = Source "scopes" $ \solver -> do
  command_ solver "(set-logic QF_LIA)"
  command_ solver "(declare-const x Int)"
  command_ solver "(declare-const y Int)"
  command_ solver "(assert (= (+ x (* 2 y)) 20))"
  command_ solver "(push 1)"
  command_ solver "(assert (= (- x y) 2))"
  _ <- command solver "(check-sat)"
  command_ solver "(pop 1)"
  command_ solver "(push 1)"
  command_ solver "(assert (= (- x y) 3))"
  _ <- command solver "(check-sat)"
  command_ solver "(pop 1)"
  return ()

sorts = Source "sorts" $ \solver -> do
  command_ solver "(set-logic QF_UF)"
  command_ solver "(declare-sort A 0)"
  command_ solver "(declare-const a A)"
  command_ solver "(declare-const b A)"
  command_ solver "(declare-const c A)"
  command_ solver "(declare-const d A)"
  command_ solver "(declare-const e A)"
  command_ solver "(assert (or (= c a)(= c b)))"
  command_ solver "(assert (or (= d a)(= d b)))"
  command_ solver "(assert (or (= e a)(= e b)))"
  command_ solver "(push 1)"
  command_ solver "(assert (distinct c d))"
  _ <- command solver "(check-sat)"
  command_ solver "(pop 1)"
  command_ solver "(push 1)"
  command_ solver "(assert (distinct c d e))"
  _ <- command solver "(check-sat)"
  command_ solver "(pop 1)"
  return ()

unsatCores = Source "unsat cores" $ \solver -> do
  command_ solver "(set-option :produce-unsat-cores true)"
  command_ solver "(set-logic QF_UF)"
  command_ solver "(declare-const p Bool)"
  command_ solver "(declare-const q Bool)"
  command_ solver "(declare-const r Bool)"
  command_ solver "(declare-const s Bool)"
  command_ solver "(declare-const t Bool)"
  command_ solver "(assert (! (=> p q) :named PQ))"
  command_ solver "(assert (! (=> q r) :named QR))"
  command_ solver "(assert (! (=> r s) :named RS))"
  command_ solver "(assert (! (=> s t) :named ST))"
  command_ solver "(assert (! (not (=> q s)) :named NQS))"
  _ <- command solver "(check-sat)"
  _ <- command solver "(get-unsat-core)"
  return ()

valuesOrModels = Source "values or models" $ \solver -> do
  command_ solver "(set-option :produce-models true)"
  command_ solver "(set-logic QF_LIA)"
  command_ solver "(declare-const x Int)"
  command_ solver "(declare-const y Int)"
  command_ solver "(assert (= (+ x (* 2 y)) 20))"
  command_ solver "(assert (= (- x y) 2))"
  _ <- command solver "(check-sat)"
  _ <- command solver "(get-value (x y))"
  _ <- command solver "(get-model)"
  return ()