{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Grisette.SymPrim.Prim.NumTests (numTests) where

import Grisette (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Term
  ( PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm),
    SupportedPrim (pevalITETerm),
    Term,
    absNumTerm,
    addNumTerm,
    conTerm,
    leOrdTerm,
    ltOrdTerm,
    mulNumTerm,
    negNumTerm,
    pevalGeOrdTerm,
    pevalGtOrdTerm,
    pevalSubNumTerm,
    signumNumTerm,
    ssymTerm,
  )
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@=?))

numTests :: Test
numTests =
  testGroup
    "Num"
    [ testGroup
        "Add"
        [ testCase "On concrete" $ do
            pevalAddNumTerm (conTerm 1 :: Term Integer) (conTerm 2) @=? conTerm 3
            pevalAddNumTerm (conTerm 1 :: Term (WordN 3)) (conTerm 2) @=? conTerm 3
            pevalAddNumTerm (conTerm 1 :: Term (IntN 3)) (conTerm 2) @=? conTerm 3,
          testCase "On left 0" $ do
            pevalAddNumTerm (conTerm 0 :: Term Integer) (ssymTerm "a") @=? ssymTerm "a",
          testCase "On right 0" $ do
            pevalAddNumTerm (ssymTerm "a") (conTerm 0 :: Term Integer) @=? ssymTerm "a",
          testCase "On left concrete" $ do
            pevalAddNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a")
              @=? addNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a" :: Term Integer),
          testCase "On right concrete" $ do
            pevalAddNumTerm (ssymTerm "a") (conTerm 1 :: Term Integer)
              @=? addNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a" :: Term Integer),
          testCase "On no concrete" $ do
            pevalAddNumTerm (ssymTerm "a") (ssymTerm "b" :: Term Integer)
              @=? addNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer),
          testCase "On left concrete and right add concrete value" $ do
            pevalAddNumTerm (conTerm 1 :: Term Integer) (pevalAddNumTerm (conTerm 2 :: Term Integer) (ssymTerm "a"))
              @=? pevalAddNumTerm (conTerm 3 :: Term Integer) (ssymTerm "a"),
          testCase "On right concrete and left add concrete value" $ do
            pevalAddNumTerm (pevalAddNumTerm (conTerm 2 :: Term Integer) (ssymTerm "a")) (conTerm 1 :: Term Integer)
              @=? pevalAddNumTerm (conTerm 3 :: Term Integer) (ssymTerm "a"),
          testCase "On left add concrete" $ do
            pevalAddNumTerm (pevalAddNumTerm (conTerm 2 :: Term Integer) (ssymTerm "a")) (ssymTerm "b")
              @=? pevalAddNumTerm (conTerm 2 :: Term Integer) (pevalAddNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On right add concrete" $ do
            pevalAddNumTerm (ssymTerm "b") (pevalAddNumTerm (conTerm 2 :: Term Integer) (ssymTerm "a"))
              @=? pevalAddNumTerm (conTerm 2 :: Term Integer) (pevalAddNumTerm (ssymTerm "b") (ssymTerm "a")),
          testCase "On both neg" $ do
            pevalAddNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term Integer) (pevalNegNumTerm $ ssymTerm "b")
              @=? pevalNegNumTerm (pevalAddNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On both mul the same concrete" $ do
            pevalAddNumTerm
              (pevalMulNumTerm (conTerm 3) (ssymTerm "a") :: Term Integer)
              (pevalMulNumTerm (conTerm 3) (ssymTerm "b"))
              @=? pevalMulNumTerm (conTerm 3) (pevalAddNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On both mul the same symbolic" $ do
            pevalAddNumTerm
              (pevalMulNumTerm (conTerm 3) (ssymTerm "a") :: Term Integer)
              (pevalMulNumTerm (conTerm 3) (ssymTerm "a"))
              @=? pevalMulNumTerm (conTerm 6) (ssymTerm "a")
            pevalAddNumTerm
              (pevalMulNumTerm (conTerm 3) (ssymTerm "a") :: Term Integer)
              (pevalMulNumTerm (conTerm 4) (ssymTerm "a"))
              @=? pevalMulNumTerm (conTerm 7) (ssymTerm "a"),
          testCase "Unfold 1" $ do
            pevalAddNumTerm
              (conTerm 3)
              (pevalITETerm (ssymTerm "a") (conTerm 1 :: Term Integer) (ssymTerm "a"))
              @=? pevalITETerm (ssymTerm "a") (conTerm 4) (pevalAddNumTerm (conTerm 3) (ssymTerm "a"))
            pevalAddNumTerm
              (pevalITETerm (ssymTerm "a") (conTerm 1 :: Term Integer) (ssymTerm "a"))
              (conTerm 3)
              @=? pevalITETerm (ssymTerm "a") (conTerm 4) (pevalAddNumTerm (ssymTerm "a") (conTerm 3))
        ],
      testGroup
        "sub"
        [ testCase "sub num should be delegated to add and neg" $ do
            pevalSubNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
              @=? pevalAddNumTerm (ssymTerm "a") (pevalNegNumTerm $ ssymTerm "b")
        ],
      testGroup
        "Neg"
        [ testCase "On concrete" $ do
            pevalNegNumTerm (conTerm 1 :: Term Integer) @=? conTerm (-1)
            pevalNegNumTerm (conTerm 1 :: Term (WordN 3)) @=? conTerm (-1),
          testCase "On Neg" $ do
            pevalNegNumTerm (pevalNegNumTerm (ssymTerm "a" :: Term Integer)) @=? ssymTerm "a",
          testCase "On Add concrete" $ do
            pevalNegNumTerm (pevalAddNumTerm (conTerm 1) (ssymTerm "a" :: Term Integer))
              @=? pevalAddNumTerm (conTerm $ -1) (pevalNegNumTerm $ ssymTerm "a"),
          testCase "On Add neg" $ do
            pevalNegNumTerm (pevalAddNumTerm (pevalNegNumTerm $ ssymTerm "a") (ssymTerm "b" :: Term Integer))
              @=? pevalAddNumTerm (ssymTerm "a") (pevalNegNumTerm $ ssymTerm "b")
            pevalNegNumTerm (pevalAddNumTerm (ssymTerm "a") (pevalNegNumTerm $ ssymTerm "b" :: Term Integer))
              @=? pevalAddNumTerm (pevalNegNumTerm $ ssymTerm "a") (ssymTerm "b"),
          testCase "On Mul concrete" $ do
            pevalNegNumTerm (pevalMulNumTerm (conTerm 3) (ssymTerm "a" :: Term Integer))
              @=? pevalMulNumTerm (conTerm $ -3) (ssymTerm "a"),
          testCase "On symbolic" $ do
            pevalNegNumTerm (ssymTerm "a" :: Term Integer)
              @=? negNumTerm (ssymTerm "a")
        ],
      testGroup
        "Mul"
        [ testCase "On both concrete" $ do
            pevalMulNumTerm (conTerm 3 :: Term Integer) (conTerm 5)
              @=? conTerm 15,
          testCase "On left 0" $ do
            pevalMulNumTerm (conTerm 0 :: Term Integer) (ssymTerm "a")
              @=? conTerm 0,
          testCase "On right 0" $ do
            pevalMulNumTerm (ssymTerm "a") (conTerm 0 :: Term Integer)
              @=? conTerm 0,
          testCase "On left 1" $ do
            pevalMulNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a")
              @=? ssymTerm "a",
          testCase "On right 1" $ do
            pevalMulNumTerm (ssymTerm "a") (conTerm 1 :: Term Integer)
              @=? ssymTerm "a",
          testCase "On left -1" $ do
            pevalMulNumTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a")
              @=? pevalNegNumTerm (ssymTerm "a"),
          testCase "On right -1" $ do
            pevalMulNumTerm (ssymTerm "a") (conTerm $ -1 :: Term Integer)
              @=? pevalNegNumTerm (ssymTerm "a"),
          testCase "On left concrete and right mul concrete symbolics" $ do
            pevalMulNumTerm (conTerm 3) (pevalMulNumTerm (conTerm 5 :: Term Integer) (ssymTerm "a"))
              @=? pevalMulNumTerm (conTerm 15) (ssymTerm "a"),
          testCase "On right concrete and left mul concrete symbolics" $ do
            pevalMulNumTerm (pevalMulNumTerm (conTerm 5 :: Term Integer) (ssymTerm "a")) (conTerm 3)
              @=? pevalMulNumTerm (conTerm 15) (ssymTerm "a"),
          testCase "On left concrete and right add concrete symbolics" $ do
            pevalMulNumTerm (conTerm 3) (pevalAddNumTerm (conTerm 5 :: Term Integer) (ssymTerm "a"))
              @=? pevalAddNumTerm (conTerm 15) (pevalMulNumTerm (conTerm 3) (ssymTerm "a")),
          testCase "On right concrete and left add concrete symbolics" $ do
            pevalMulNumTerm (pevalAddNumTerm (conTerm 5 :: Term Integer) (ssymTerm "a")) (conTerm 3)
              @=? pevalAddNumTerm (conTerm 15) (pevalMulNumTerm (conTerm 3) (ssymTerm "a")),
          testCase "On left concrete and right neg" $ do
            pevalMulNumTerm (conTerm 3 :: Term Integer) (pevalNegNumTerm (ssymTerm "a"))
              @=? pevalMulNumTerm (conTerm $ -3) (ssymTerm "a"),
          testCase "On left mul concrete symbolics" $ do
            pevalMulNumTerm (pevalMulNumTerm (conTerm 3 :: Term Integer) (ssymTerm "a")) (ssymTerm "b")
              @=? pevalMulNumTerm (conTerm 3) (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On right mul concrete symbolics" $ do
            pevalMulNumTerm (ssymTerm "b") (pevalMulNumTerm (conTerm 3 :: Term Integer) (ssymTerm "a"))
              @=? pevalMulNumTerm (conTerm 3) (pevalMulNumTerm (ssymTerm "b") (ssymTerm "a")),
          testCase "On left neg" $ do
            pevalMulNumTerm (pevalNegNumTerm $ ssymTerm "a") (ssymTerm "b" :: Term Integer)
              @=? pevalNegNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On right neg" $ do
            pevalMulNumTerm (ssymTerm "a") (pevalNegNumTerm $ ssymTerm "b" :: Term Integer)
              @=? pevalNegNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On right concrete and left neg" $ do
            pevalMulNumTerm (pevalNegNumTerm (ssymTerm "a")) (conTerm 3 :: Term Integer)
              @=? pevalMulNumTerm (conTerm $ -3) (ssymTerm "a"),
          testCase "On left concrete" $ do
            pevalMulNumTerm (conTerm 3 :: Term Integer) (ssymTerm "a")
              @=? mulNumTerm
                (conTerm 3 :: Term Integer)
                (ssymTerm "a" :: Term Integer),
          testCase "On right concrete" $ do
            pevalMulNumTerm (ssymTerm "a") (conTerm 3 :: Term Integer)
              @=? mulNumTerm
                (conTerm 3 :: Term Integer)
                (ssymTerm "a" :: Term Integer),
          testCase "On no concrete" $ do
            pevalMulNumTerm (ssymTerm "a") (ssymTerm "b" :: Term Integer)
              @=? mulNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer),
          testCase "Unfold 1" $ do
            pevalMulNumTerm
              (conTerm 3)
              (pevalITETerm (ssymTerm "a") (conTerm 5 :: Term Integer) (ssymTerm "a"))
              @=? pevalITETerm (ssymTerm "a") (conTerm 15) (pevalMulNumTerm (conTerm 3) (ssymTerm "a"))
            pevalMulNumTerm
              (pevalITETerm (ssymTerm "a") (conTerm 5 :: Term Integer) (ssymTerm "a"))
              (conTerm 3)
              @=? pevalITETerm (ssymTerm "a") (conTerm 15) (pevalMulNumTerm (ssymTerm "a") (conTerm 3))
        ],
      testGroup
        "Abs"
        [ testCase "On concrete" $ do
            pevalAbsNumTerm (conTerm 10 :: Term Integer) @=? conTerm 10
            pevalAbsNumTerm (conTerm $ -10 :: Term Integer) @=? conTerm 10,
          testCase "On Neg Integer" $ do
            pevalAbsNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term Integer) @=? pevalAbsNumTerm (ssymTerm "a"),
          testCase "On Neg BV" $ do
            pevalAbsNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (IntN 5)) @=? pevalAbsNumTerm (ssymTerm "a")
            pevalAbsNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (WordN 5)) @=? negNumTerm (ssymTerm "a"),
          testCase "On Abs Integer" $ do
            pevalAbsNumTerm (pevalAbsNumTerm $ ssymTerm "a" :: Term Integer) @=? pevalAbsNumTerm (ssymTerm "a"),
          testCase "On Abs BV" $ do
            pevalAbsNumTerm (pevalAbsNumTerm $ ssymTerm "a" :: Term (IntN 5)) @=? pevalAbsNumTerm (ssymTerm "a")
            pevalAbsNumTerm (pevalAbsNumTerm $ ssymTerm "a" :: Term (WordN 5)) @=? ssymTerm "a",
          testCase "On Mul Integer" $ do
            pevalAbsNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term Integer)
              @=? pevalMulNumTerm (pevalAbsNumTerm (ssymTerm "a")) (pevalAbsNumTerm (ssymTerm "b")),
          testCase "On Mul BV" $ do
            pevalAbsNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (IntN 5))
              @=? absNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (IntN 5))
            pevalAbsNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (WordN 5))
              @=? pevalMulNumTerm (ssymTerm "a") (ssymTerm "b"),
          testCase "On symbolic Integer" $ do
            pevalAbsNumTerm (ssymTerm "a" :: Term Integer)
              @=? absNumTerm (ssymTerm "a"),
          testCase "On symbolic BV" $ do
            pevalAbsNumTerm (ssymTerm "a" :: Term (IntN 5)) @=? absNumTerm (ssymTerm "a")
            pevalAbsNumTerm (ssymTerm "a" :: Term (WordN 5)) @=? ssymTerm "a"
        ],
      testGroup
        "Signum"
        [ testCase "On concrete" $ do
            pevalSignumNumTerm (conTerm 10 :: Term Integer) @=? conTerm 1
            pevalSignumNumTerm (conTerm 0 :: Term Integer) @=? conTerm 0
            pevalSignumNumTerm (conTerm $ -10 :: Term Integer) @=? conTerm (-1),
          testCase "On Neg Integer" $ do
            pevalSignumNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term Integer)
              @=? pevalNegNumTerm (pevalSignumNumTerm $ ssymTerm "a"),
          testCase "On Neg BV" $ do
            pevalSignumNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (IntN 5))
              @=? signumNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (IntN 5))
            pevalSignumNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (WordN 5))
              @=? signumNumTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (WordN 5)),
          testCase "On Mul Integer" $ do
            pevalSignumNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term Integer)
              @=? pevalMulNumTerm (pevalSignumNumTerm $ ssymTerm "a") (pevalSignumNumTerm $ ssymTerm "b"),
          testCase "On Mul BV" $ do
            pevalSignumNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (IntN 5))
              @=? signumNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (IntN 5))
            pevalSignumNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (WordN 5))
              @=? signumNumTerm (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (WordN 5)),
          testCase "On symbolics" $ do
            pevalSignumNumTerm (ssymTerm "a" :: Term Integer)
              @=? signumNumTerm (ssymTerm "a")
        ],
      let concSignedBV :: Integer -> Term (IntN 5) = conTerm . fromInteger
          concUnsignedBV :: Integer -> Term (WordN 5) = conTerm . fromInteger
       in testGroup
            "Lt"
            [ testCase "On both concrete" $ do
                pevalLtOrdTerm (conTerm 1 :: Term Integer) (conTerm 2) @=? conTerm True
                pevalLtOrdTerm (conTerm 2 :: Term Integer) (conTerm 2) @=? conTerm False
                pevalLtOrdTerm (conTerm 3 :: Term Integer) (conTerm 2) @=? conTerm False
                pevalLtOrdTerm (conTerm 1 :: Term (IntN 2)) (conTerm 0) @=? conTerm False
                pevalLtOrdTerm (conTerm 2 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLtOrdTerm (conTerm 3 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLtOrdTerm (conTerm 1 :: Term (WordN 2)) (conTerm 2) @=? conTerm True
                pevalLtOrdTerm (conTerm 2 :: Term (WordN 2)) (conTerm 2) @=? conTerm False
                pevalLtOrdTerm (conTerm 3 :: Term (WordN 2)) (conTerm 2) @=? conTerm False,
              testCase "On left constant and right add concrete Integers" $ do
                pevalLtOrdTerm (conTerm 1 :: Term Integer) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? pevalLtOrdTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a"),
              testCase "On right constant left add concrete Integers" $ do
                pevalLtOrdTerm (pevalAddNumTerm (conTerm 2) (ssymTerm "a")) (conTerm 1 :: Term Integer)
                  @=? pevalLtOrdTerm (conTerm 1 :: Term Integer) (pevalNegNumTerm $ ssymTerm "a"),
              testCase "On right constant Integers" $ do
                pevalLtOrdTerm (ssymTerm "a") (conTerm 1 :: Term Integer)
                  @=? pevalLtOrdTerm (conTerm $ -1 :: Term Integer) (pevalNegNumTerm $ ssymTerm "a"),
              testCase "On right constant and left neg Integers" $ do
                pevalLtOrdTerm (pevalNegNumTerm $ ssymTerm "a") (conTerm 1 :: Term Integer)
                  @=? pevalLtOrdTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a"),
              testCase "On left add concrete Integers" $ do
                pevalLtOrdTerm (pevalAddNumTerm (conTerm 2) (ssymTerm "a")) (ssymTerm "b" :: Term Integer)
                  @=? pevalLtOrdTerm (conTerm 2 :: Term Integer) (pevalAddNumTerm (ssymTerm "b") (pevalNegNumTerm $ ssymTerm "a")),
              testCase "On right add concrete Integers" $ do
                pevalLtOrdTerm (ssymTerm "b" :: Term Integer) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? pevalLtOrdTerm (conTerm $ -2 :: Term Integer) (pevalAddNumTerm (ssymTerm "a") (pevalNegNumTerm $ ssymTerm "b")),
              testCase "On left constant and right add concrete BVs should not be simplified" $ do
                pevalLtOrdTerm (concSignedBV 1) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? ltOrdTerm (concSignedBV 1) (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                pevalLtOrdTerm (concUnsignedBV 1) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? ltOrdTerm (concUnsignedBV 1) (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")),
              testCase "On right constant and left add concrete BVs should not be simplified" $ do
                pevalLtOrdTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (conTerm 1)
                  @=? ltOrdTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (concSignedBV 1)
                pevalLtOrdTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (conTerm 1)
                  @=? ltOrdTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (concUnsignedBV 1),
              testCase "On right constant BVs should not be simplified" $ do
                pevalLtOrdTerm (ssymTerm "a") (concSignedBV 1)
                  @=? ltOrdTerm (ssymTerm "a" :: Term (IntN 5)) (concSignedBV 1)
                pevalLtOrdTerm (ssymTerm "a") (concUnsignedBV 1)
                  @=? ltOrdTerm (ssymTerm "a" :: Term (WordN 5)) (concUnsignedBV 1),
              testCase "On right constant and left neg BVs should not be simplified" $ do
                pevalLtOrdTerm (pevalNegNumTerm $ ssymTerm "a") (concSignedBV 1)
                  @=? ltOrdTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (IntN 5)) (concSignedBV 1)
                pevalLtOrdTerm (pevalNegNumTerm $ ssymTerm "a") (concUnsignedBV 1)
                  @=? ltOrdTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (WordN 5)) (concUnsignedBV 1),
              testCase "On left add concrete BVs should not be simplified" $ do
                pevalLtOrdTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (ssymTerm "b")
                  @=? ltOrdTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (ssymTerm "b" :: Term (IntN 5))
                pevalLtOrdTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (ssymTerm "b")
                  @=? ltOrdTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (ssymTerm "b" :: Term (WordN 5)),
              testCase "On right add concrete BVs should not be simplified" $ do
                pevalLtOrdTerm (ssymTerm "b") (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                  @=? ltOrdTerm
                    (ssymTerm "b" :: Term (IntN 5))
                    (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                pevalLtOrdTerm (ssymTerm "b") (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a"))
                  @=? ltOrdTerm
                    (ssymTerm "b" :: Term (WordN 5))
                    (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")),
              testCase "On symbolic" $ do
                pevalLtOrdTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                  @=? ltOrdTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer)
            ],
      let concSignedBV :: Integer -> Term (IntN 5) = conTerm . fromInteger
          concUnsignedBV :: Integer -> Term (WordN 5) = conTerm . fromInteger
       in testGroup
            "Le"
            [ testCase "On both concrete" $ do
                pevalLeOrdTerm (conTerm 1 :: Term Integer) (conTerm 2) @=? conTerm True
                pevalLeOrdTerm (conTerm 2 :: Term Integer) (conTerm 2) @=? conTerm True
                pevalLeOrdTerm (conTerm 3 :: Term Integer) (conTerm 2) @=? conTerm False
                pevalLeOrdTerm (conTerm 0 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLeOrdTerm (conTerm 1 :: Term (IntN 2)) (conTerm 0) @=? conTerm False
                pevalLeOrdTerm (conTerm 2 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLeOrdTerm (conTerm 3 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLeOrdTerm (conTerm 1 :: Term (WordN 2)) (conTerm 2) @=? conTerm True
                pevalLeOrdTerm (conTerm 2 :: Term (WordN 2)) (conTerm 2) @=? conTerm True
                pevalLeOrdTerm (conTerm 3 :: Term (WordN 2)) (conTerm 2) @=? conTerm False,
              testCase "On left constant and right add concrete Integers" $ do
                pevalLeOrdTerm (conTerm 1 :: Term Integer) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? pevalLeOrdTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a"),
              testCase "On right constant and left add concrete Integers" $ do
                pevalLeOrdTerm (pevalAddNumTerm (conTerm 2) (ssymTerm "a")) (conTerm 1 :: Term Integer)
                  @=? pevalLeOrdTerm (conTerm 1 :: Term Integer) (pevalNegNumTerm $ ssymTerm "a"),
              testCase "On right constant Integers" $ do
                pevalLeOrdTerm (ssymTerm "a") (conTerm 1 :: Term Integer)
                  @=? pevalLeOrdTerm (conTerm $ -1 :: Term Integer) (pevalNegNumTerm $ ssymTerm "a"),
              testCase "On right constant left neg Integers" $ do
                pevalLeOrdTerm (pevalNegNumTerm $ ssymTerm "a") (conTerm 1 :: Term Integer)
                  @=? pevalLeOrdTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a"),
              testCase "On left add concrete Integers" $ do
                pevalLeOrdTerm (pevalAddNumTerm (conTerm 2) (ssymTerm "a")) (ssymTerm "b" :: Term Integer)
                  @=? pevalLeOrdTerm (conTerm 2 :: Term Integer) (pevalAddNumTerm (ssymTerm "b") (pevalNegNumTerm $ ssymTerm "a")),
              testCase "On right add concrete Integers" $ do
                pevalLeOrdTerm (ssymTerm "b" :: Term Integer) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? pevalLeOrdTerm (conTerm $ -2 :: Term Integer) (pevalAddNumTerm (ssymTerm "a") (pevalNegNumTerm $ ssymTerm "b")),
              testCase "On left constant and right add concrete BVs should not be simplified" $ do
                pevalLeOrdTerm (concSignedBV 1) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? leOrdTerm (concSignedBV 1) (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                pevalLeOrdTerm (concUnsignedBV 1) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? leOrdTerm (concUnsignedBV 1) (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")),
              testCase "On right constant and left add concrete BVs should not be simplified" $ do
                pevalLeOrdTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (conTerm 1)
                  @=? leOrdTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (concSignedBV 1)
                pevalLeOrdTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (conTerm 1)
                  @=? leOrdTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (concUnsignedBV 1),
              testCase "On right constant BVs should not be simplified" $ do
                pevalLeOrdTerm (ssymTerm "a") (concSignedBV 1)
                  @=? leOrdTerm (ssymTerm "a" :: Term (IntN 5)) (concSignedBV 1)
                pevalLeOrdTerm (ssymTerm "a") (concUnsignedBV 1)
                  @=? leOrdTerm (ssymTerm "a" :: Term (WordN 5)) (concUnsignedBV 1),
              testCase "On right constant and left neg BVs should not be simplified" $ do
                pevalLeOrdTerm (pevalNegNumTerm $ ssymTerm "a") (concSignedBV 1)
                  @=? leOrdTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (IntN 5)) (concSignedBV 1)
                pevalLeOrdTerm (pevalNegNumTerm $ ssymTerm "a") (concUnsignedBV 1)
                  @=? leOrdTerm (pevalNegNumTerm $ ssymTerm "a" :: Term (WordN 5)) (concUnsignedBV 1),
              testCase "On left add concrete BVs should not be simplified" $ do
                pevalLeOrdTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (ssymTerm "b")
                  @=? leOrdTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (ssymTerm "b" :: Term (IntN 5))
                pevalLeOrdTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (ssymTerm "b")
                  @=? leOrdTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (ssymTerm "b" :: Term (WordN 5)),
              testCase "Lt on right add concrete BVs should not be simplified" $ do
                pevalLeOrdTerm (ssymTerm "b") (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                  @=? leOrdTerm
                    (ssymTerm "b" :: Term (IntN 5))
                    (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                pevalLeOrdTerm (ssymTerm "b") (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a"))
                  @=? leOrdTerm
                    (ssymTerm "b" :: Term (WordN 5))
                    (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")),
              testCase "On symbolic" $ do
                pevalLeOrdTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                  @=? leOrdTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer)
            ],
      testCase "Gt should be delegated to Lt" $
        pevalGtOrdTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
          @=? pevalLtOrdTerm (ssymTerm "b" :: Term Integer) (ssymTerm "a"),
      testCase "Ge should be delegated to Le" $ do
        pevalGeOrdTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
          @=? pevalLeOrdTerm (ssymTerm "b" :: Term Integer) (ssymTerm "a")
    ]