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

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 = map (map toLower)
                        [ "Int", "Real", "List", "Array", "Bool", "FP", "FloatingPoint", "fp", "String"
                        , "!", "_", "as", "BINARY", "DECIMAL", "exists", "HEXADECIMAL", "forall", "let", "NUMERAL", "par", "STRING", "CHAR"
                        , "assert", "check-sat", "check-sat-assuming", "declare-const", "declare-fun", "declare-sort", "define-fun", "define-fun-rec"
                        , "define-sort", "echo", "exit", "get-assertions", "get-assignment", "get-info", "get-model", "get-option", "get-proof", "get-unsat-assumptions"
                        , "get-unsat-core", "get-value", "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option", "match"
                        --
                        -- The following are most likely Z3 specific
                        , "interval", "assert-soft"
                        ]