{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}
module SMTLIB.Backends.Tests.Sources (Source (..), sources) where
import SMTLIB.Backends
data Source = Source
{
Source -> String
name :: String,
Source -> Solver -> IO ()
run :: Solver -> IO ()
}
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 ()