-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.SMT.SMTLibNames
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- SMTLib Reserved names
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.SMT.SMTLibNames where

import Data.Char (toLower)

-- | Names reserved by SMTLib. This list is current as of Dec 6 2015; but of course
-- there's no guarantee it'll stay that way.
smtLibReservedNames :: [String]
smtLibReservedNames :: [String]
smtLibReservedNames = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower)
                        [ String
"Int", String
"Real", String
"List", String
"Array", String
"Bool", String
"FP", String
"FloatingPoint", String
"fp", String
"String"
                        , String
"!", String
"_", String
"as", String
"BINARY", String
"DECIMAL", String
"exists", String
"HEXADECIMAL", String
"forall", String
"let", String
"NUMERAL", String
"par", String
"STRING", String
"CHAR"
                        , String
"assert", String
"check-sat", String
"check-sat-assuming", String
"declare-const", String
"declare-fun", String
"declare-sort", String
"define-fun", String
"define-fun-rec"
                        , String
"define-sort", String
"echo", String
"exit", String
"get-assertions", String
"get-assignment", String
"get-info", String
"get-model", String
"get-option", String
"get-proof", String
"get-unsat-assumptions"
                        , String
"get-unsat-core", String
"get-value", String
"pop", String
"push", String
"reset", String
"reset-assertions", String
"set-info", String
"set-logic", String
"set-option", String
"match"
                        --
                        -- The following are most likely Z3 specific
                        , String
"interval", String
"assert-soft"
                        ]