--- This module defines some auxiliary operation to construct
--- SMT-LIB formulas.

module XFD.SMTLib.Build where

import XFD.SMTLib.Types

declareConst :: String -> String -> Command
declareConst n s = DeclareConst n (SortId (ISymbol s))

declareInt :: String -> Command
declareInt = flip declareConst "Int"

termSpecConstNum :: Int -> Term
termSpecConstNum i = TermSpecConstant (specConstNum i)

specConstNum :: Int -> SpecConstant
specConstNum i = SpecConstantNumeral i

termQIdent  :: String -> Term
termQIdent sym = TermQualIdentifier (qIdent sym)

termQIdentT :: String -> [Term] -> Term
termQIdentT sym ts = TermQualIdentifierT (qIdent sym) ts

qIdent :: String -> QualIdentifier
qIdent sym = QIdentifier $ ident sym

ident :: String -> Identifier
ident sym = ISymbol sym