import Text.ParserCombinators.Parsec
import TRS
import TRSParser

-- Data structures for SMT inputs.

data Exp = Var String
         | Val Int
         | Plus [Exp]
         | Times [Exp]
         deriving Eq

instance Show Exp where

data Formula = Gt Exp Exp
             | Geq Exp Exp

instance Show Formula where

data Command =
     DeclareInt String
   | Assert Formula
   | CheckSat
   | GetValue [String]

instance Show Command where

type SMTInput = [Command]

showSMTInput :: SMTInput -> String
showSMTInput = undefined

-- Z3 outputs.

-- sat ((x 1) (y 2)) corresponds to Just [("x", 1), ("y", 2)]
-- unsat corresponds to Nothing
type Z3Output = Maybe [(String, Int)]

parseZ3Output :: Parser Z3Output
parseZ3Output = undefined

-- Assume that every interpretation function f_A is defined as:
--
--    f_A(x_1,...,x_n) = a_0 + a_1 x_1 + ... + a_n x_n
--
-- coefficient t x returns the coefficient of x in the interpretation of t.
-- E.g., coefficient (F "a" [F "s" [V "x"], V "x"]) "x" returns
-- the expression that represents (+ (* a1 s1) a2).
coefficient :: Term -> String -> Exp
coefficient = undefined

-- constraint t returns the constant part of the interpretation of t.
-- E.g., constant (F "a" [F "s" [V "x"], V "x"]) returns
-- the expression that represents (+ a_0 (* a_1 s_0)).
constant :: Term -> Exp
constant = undefined

-- constraints [(l_1,r_1),...,(l_n,r_n)] returns a formula that represents
-- l_1 >_A r_1 and ... and l_n >_A r_n.
constraints :: TRS -> Formula
constraints = undefined

-- main outputs "YES" if Z3 returns sat, and "MAYBE" otherwise.
main :: IO ()
main = undefined