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

module Grisette.IR.SymPrim.Data.Prim.NumTests where

import Grisette.IR.SymPrim.Data.BV
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
import Test.Tasty
import Test.Tasty.HUnit

numTests :: TestTree
numTests =
  testGroup
    "NumTests"
    [ 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 uminus" $ do
            pevalAddNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term Integer) (pevalUMinusNumTerm $ ssymTerm "b")
              @=? pevalUMinusNumTerm (pevalAddNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On both times the same concrete" $ do
            pevalAddNumTerm
              (pevalTimesNumTerm (conTerm 3) (ssymTerm "a") :: Term Integer)
              (pevalTimesNumTerm (conTerm 3) (ssymTerm "b"))
              @=? pevalTimesNumTerm (conTerm 3) (pevalAddNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On both times the same symbolic" $ do
            pevalAddNumTerm
              (pevalTimesNumTerm (conTerm 3) (ssymTerm "a") :: Term Integer)
              (pevalTimesNumTerm (conTerm 3) (ssymTerm "a"))
              @=? pevalTimesNumTerm (conTerm 6) (ssymTerm "a")
            pevalAddNumTerm
              (pevalTimesNumTerm (conTerm 3) (ssymTerm "a") :: Term Integer)
              (pevalTimesNumTerm (conTerm 4) (ssymTerm "a"))
              @=? pevalTimesNumTerm (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
        "minus"
        [ testCase "minus num should be delegated to add and uminus" $ do
            pevalMinusNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
              @=? pevalAddNumTerm (ssymTerm "a") (pevalUMinusNumTerm $ ssymTerm "b")
        ],
      testGroup
        "UMinus"
        [ testCase "On concrete" $ do
            pevalUMinusNumTerm (conTerm 1 :: Term Integer) @=? conTerm (-1)
            pevalUMinusNumTerm (conTerm 1 :: Term (WordN 3)) @=? conTerm (-1),
          testCase "On UMinus" $ do
            pevalUMinusNumTerm (pevalUMinusNumTerm (ssymTerm "a" :: Term Integer)) @=? ssymTerm "a",
          testCase "On Add concrete" $ do
            pevalUMinusNumTerm (pevalAddNumTerm (conTerm 1) (ssymTerm "a" :: Term Integer))
              @=? pevalAddNumTerm (conTerm $ -1) (pevalUMinusNumTerm $ ssymTerm "a"),
          testCase "On Add uminus" $ do
            pevalUMinusNumTerm (pevalAddNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (ssymTerm "b" :: Term Integer))
              @=? pevalAddNumTerm (ssymTerm "a") (pevalUMinusNumTerm $ ssymTerm "b")
            pevalUMinusNumTerm (pevalAddNumTerm (ssymTerm "a") (pevalUMinusNumTerm $ ssymTerm "b" :: Term Integer))
              @=? pevalAddNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (ssymTerm "b"),
          testCase "On Times concrete" $ do
            pevalUMinusNumTerm (pevalTimesNumTerm (conTerm 3) (ssymTerm "a" :: Term Integer))
              @=? pevalTimesNumTerm (conTerm $ -3) (ssymTerm "a"),
          testCase "On symbolic" $ do
            pevalUMinusNumTerm (ssymTerm "a" :: Term Integer)
              @=? uminusNumTerm (ssymTerm "a")
        ],
      testGroup
        "Times"
        [ testCase "On both concrete" $ do
            pevalTimesNumTerm (conTerm 3 :: Term Integer) (conTerm 5)
              @=? conTerm 15,
          testCase "On left 0" $ do
            pevalTimesNumTerm (conTerm 0 :: Term Integer) (ssymTerm "a")
              @=? conTerm 0,
          testCase "On right 0" $ do
            pevalTimesNumTerm (ssymTerm "a") (conTerm 0 :: Term Integer)
              @=? conTerm 0,
          testCase "On left 1" $ do
            pevalTimesNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a")
              @=? ssymTerm "a",
          testCase "On right 1" $ do
            pevalTimesNumTerm (ssymTerm "a") (conTerm 1 :: Term Integer)
              @=? ssymTerm "a",
          testCase "On left -1" $ do
            pevalTimesNumTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a")
              @=? pevalUMinusNumTerm (ssymTerm "a"),
          testCase "On right -1" $ do
            pevalTimesNumTerm (ssymTerm "a") (conTerm $ -1 :: Term Integer)
              @=? pevalUMinusNumTerm (ssymTerm "a"),
          testCase "On left concrete and right times concrete symbolics" $ do
            pevalTimesNumTerm (conTerm 3) (pevalTimesNumTerm (conTerm 5 :: Term Integer) (ssymTerm "a"))
              @=? pevalTimesNumTerm (conTerm 15) (ssymTerm "a"),
          testCase "On right concrete and left times concrete symbolics" $ do
            pevalTimesNumTerm (pevalTimesNumTerm (conTerm 5 :: Term Integer) (ssymTerm "a")) (conTerm 3)
              @=? pevalTimesNumTerm (conTerm 15) (ssymTerm "a"),
          testCase "On left concrete and right add concrete symbolics" $ do
            pevalTimesNumTerm (conTerm 3) (pevalAddNumTerm (conTerm 5 :: Term Integer) (ssymTerm "a"))
              @=? pevalAddNumTerm (conTerm 15) (pevalTimesNumTerm (conTerm 3) (ssymTerm "a")),
          testCase "On right concrete and left add concrete symbolics" $ do
            pevalTimesNumTerm (pevalAddNumTerm (conTerm 5 :: Term Integer) (ssymTerm "a")) (conTerm 3)
              @=? pevalAddNumTerm (conTerm 15) (pevalTimesNumTerm (conTerm 3) (ssymTerm "a")),
          testCase "On left concrete and right uminus" $ do
            pevalTimesNumTerm (conTerm 3 :: Term Integer) (pevalUMinusNumTerm (ssymTerm "a"))
              @=? pevalTimesNumTerm (conTerm $ -3) (ssymTerm "a"),
          testCase "On left times concrete symbolics" $ do
            pevalTimesNumTerm (pevalTimesNumTerm (conTerm 3 :: Term Integer) (ssymTerm "a")) (ssymTerm "b")
              @=? pevalTimesNumTerm (conTerm 3) (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On right times concrete symbolics" $ do
            pevalTimesNumTerm (ssymTerm "b") (pevalTimesNumTerm (conTerm 3 :: Term Integer) (ssymTerm "a"))
              @=? pevalTimesNumTerm (conTerm 3) (pevalTimesNumTerm (ssymTerm "b") (ssymTerm "a")),
          testCase "On left uminus" $ do
            pevalTimesNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (ssymTerm "b" :: Term Integer)
              @=? pevalUMinusNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On right uminus" $ do
            pevalTimesNumTerm (ssymTerm "a") (pevalUMinusNumTerm $ ssymTerm "b" :: Term Integer)
              @=? pevalUMinusNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On right concrete and left uminus" $ do
            pevalTimesNumTerm (pevalUMinusNumTerm (ssymTerm "a")) (conTerm 3 :: Term Integer)
              @=? pevalTimesNumTerm (conTerm $ -3) (ssymTerm "a"),
          testCase "On left concrete" $ do
            pevalTimesNumTerm (conTerm 3 :: Term Integer) (ssymTerm "a")
              @=? timesNumTerm
                (conTerm 3 :: Term Integer)
                (ssymTerm "a" :: Term Integer),
          testCase "On right concrete" $ do
            pevalTimesNumTerm (ssymTerm "a") (conTerm 3 :: Term Integer)
              @=? timesNumTerm
                (conTerm 3 :: Term Integer)
                (ssymTerm "a" :: Term Integer),
          testCase "On no concrete" $ do
            pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b" :: Term Integer)
              @=? timesNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer),
          testCase "Unfold 1" $ do
            pevalTimesNumTerm
              (conTerm 3)
              (pevalITETerm (ssymTerm "a") (conTerm 5 :: Term Integer) (ssymTerm "a"))
              @=? pevalITETerm (ssymTerm "a") (conTerm 15) (pevalTimesNumTerm (conTerm 3) (ssymTerm "a"))
            pevalTimesNumTerm
              (pevalITETerm (ssymTerm "a") (conTerm 5 :: Term Integer) (ssymTerm "a"))
              (conTerm 3)
              @=? pevalITETerm (ssymTerm "a") (conTerm 15) (pevalTimesNumTerm (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 UMinus" $ do
            pevalAbsNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term Integer) @=? pevalAbsNumTerm (ssymTerm "a"),
          testCase "On Abs" $ do
            pevalAbsNumTerm (pevalAbsNumTerm $ ssymTerm "a" :: Term Integer) @=? pevalAbsNumTerm (ssymTerm "a"),
          testCase "On Times Integer" $ do
            pevalAbsNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term Integer)
              @=? pevalTimesNumTerm (pevalAbsNumTerm (ssymTerm "a")) (pevalAbsNumTerm (ssymTerm "b")),
          testCase "On Times BV" $ do
            pevalAbsNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (IntN 5))
              @=? absNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (IntN 5))
            pevalAbsNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (WordN 5))
              @=? absNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (WordN 5)),
          testCase "On symbolic" $ do
            pevalAbsNumTerm (ssymTerm "a" :: Term Integer)
              @=? absNumTerm (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 UMinus Integer" $ do
            pevalSignumNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term Integer)
              @=? pevalUMinusNumTerm (pevalSignumNumTerm $ ssymTerm "a"),
          testCase "On UMinus BV" $ do
            pevalSignumNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term (IntN 5))
              @=? signumNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term (IntN 5))
            pevalSignumNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term (WordN 5))
              @=? signumNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term (WordN 5)),
          testCase "On Times Integer" $ do
            pevalSignumNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term Integer)
              @=? pevalTimesNumTerm (pevalSignumNumTerm $ ssymTerm "a") (pevalSignumNumTerm $ ssymTerm "b"),
          testCase "On Times BV" $ do
            pevalSignumNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (IntN 5))
              @=? signumNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (IntN 5))
            pevalSignumNumTerm (pevalTimesNumTerm (ssymTerm "a") (ssymTerm "b") :: Term (WordN 5))
              @=? signumNumTerm (pevalTimesNumTerm (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
                pevalLtNumTerm (conTerm 1 :: Term Integer) (conTerm 2) @=? conTerm True
                pevalLtNumTerm (conTerm 2 :: Term Integer) (conTerm 2) @=? conTerm False
                pevalLtNumTerm (conTerm 3 :: Term Integer) (conTerm 2) @=? conTerm False
                pevalLtNumTerm (conTerm 1 :: Term (IntN 2)) (conTerm 0) @=? conTerm False
                pevalLtNumTerm (conTerm 2 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLtNumTerm (conTerm 3 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLtNumTerm (conTerm 1 :: Term (WordN 2)) (conTerm 2) @=? conTerm True
                pevalLtNumTerm (conTerm 2 :: Term (WordN 2)) (conTerm 2) @=? conTerm False
                pevalLtNumTerm (conTerm 3 :: Term (WordN 2)) (conTerm 2) @=? conTerm False,
              testCase "On left constant and right add concrete Integers" $ do
                pevalLtNumTerm (conTerm 1 :: Term Integer) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? pevalLtNumTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a"),
              testCase "On right constant left add concrete Integers" $ do
                pevalLtNumTerm (pevalAddNumTerm (conTerm 2) (ssymTerm "a")) (conTerm 1 :: Term Integer)
                  @=? pevalLtNumTerm (conTerm 1 :: Term Integer) (pevalUMinusNumTerm $ ssymTerm "a"),
              testCase "On right constant Integers" $ do
                pevalLtNumTerm (ssymTerm "a") (conTerm 1 :: Term Integer)
                  @=? pevalLtNumTerm (conTerm $ -1 :: Term Integer) (pevalUMinusNumTerm $ ssymTerm "a"),
              testCase "On right constant and left uminus Integers" $ do
                pevalLtNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (conTerm 1 :: Term Integer)
                  @=? pevalLtNumTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a"),
              testCase "On left add concrete Integers" $ do
                pevalLtNumTerm (pevalAddNumTerm (conTerm 2) (ssymTerm "a")) (ssymTerm "b" :: Term Integer)
                  @=? pevalLtNumTerm (conTerm 2 :: Term Integer) (pevalAddNumTerm (ssymTerm "b") (pevalUMinusNumTerm $ ssymTerm "a")),
              testCase "On right add concrete Integers" $ do
                pevalLtNumTerm (ssymTerm "b" :: Term Integer) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? pevalLtNumTerm (conTerm $ -2 :: Term Integer) (pevalAddNumTerm (ssymTerm "a") (pevalUMinusNumTerm $ ssymTerm "b")),
              testCase "On left constant and right add concrete BVs should not be simplified" $ do
                pevalLtNumTerm (concSignedBV 1) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? ltNumTerm (concSignedBV 1) (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                pevalLtNumTerm (concUnsignedBV 1) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? ltNumTerm (concUnsignedBV 1) (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")),
              testCase "On right constant and left add concrete BVs should not be simplified" $ do
                pevalLtNumTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (conTerm 1)
                  @=? ltNumTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (concSignedBV 1)
                pevalLtNumTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (conTerm 1)
                  @=? ltNumTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (concUnsignedBV 1),
              testCase "On right constant BVs should not be simplified" $ do
                pevalLtNumTerm (ssymTerm "a") (concSignedBV 1)
                  @=? ltNumTerm (ssymTerm "a" :: Term (IntN 5)) (concSignedBV 1)
                pevalLtNumTerm (ssymTerm "a") (concUnsignedBV 1)
                  @=? ltNumTerm (ssymTerm "a" :: Term (WordN 5)) (concUnsignedBV 1),
              testCase "On right constant and left uminus BVs should not be simplified" $ do
                pevalLtNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (concSignedBV 1)
                  @=? ltNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term (IntN 5)) (concSignedBV 1)
                pevalLtNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (concUnsignedBV 1)
                  @=? ltNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term (WordN 5)) (concUnsignedBV 1),
              testCase "On left add concrete BVs should not be simplified" $ do
                pevalLtNumTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (ssymTerm "b")
                  @=? ltNumTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (ssymTerm "b" :: Term (IntN 5))
                pevalLtNumTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (ssymTerm "b")
                  @=? ltNumTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (ssymTerm "b" :: Term (WordN 5)),
              testCase "On right add concrete BVs should not be simplified" $ do
                pevalLtNumTerm (ssymTerm "b") (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                  @=? ltNumTerm
                    (ssymTerm "b" :: Term (IntN 5))
                    (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                pevalLtNumTerm (ssymTerm "b") (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a"))
                  @=? ltNumTerm
                    (ssymTerm "b" :: Term (WordN 5))
                    (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")),
              testCase "On symbolic" $ do
                pevalLtNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                  @=? ltNumTerm (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
                pevalLeNumTerm (conTerm 1 :: Term Integer) (conTerm 2) @=? conTerm True
                pevalLeNumTerm (conTerm 2 :: Term Integer) (conTerm 2) @=? conTerm True
                pevalLeNumTerm (conTerm 3 :: Term Integer) (conTerm 2) @=? conTerm False
                pevalLeNumTerm (conTerm 0 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLeNumTerm (conTerm 1 :: Term (IntN 2)) (conTerm 0) @=? conTerm False
                pevalLeNumTerm (conTerm 2 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLeNumTerm (conTerm 3 :: Term (IntN 2)) (conTerm 0) @=? conTerm True
                pevalLeNumTerm (conTerm 1 :: Term (WordN 2)) (conTerm 2) @=? conTerm True
                pevalLeNumTerm (conTerm 2 :: Term (WordN 2)) (conTerm 2) @=? conTerm True
                pevalLeNumTerm (conTerm 3 :: Term (WordN 2)) (conTerm 2) @=? conTerm False,
              testCase "On left constant and right add concrete Integers" $ do
                pevalLeNumTerm (conTerm 1 :: Term Integer) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? pevalLeNumTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a"),
              testCase "On right constant and left add concrete Integers" $ do
                pevalLeNumTerm (pevalAddNumTerm (conTerm 2) (ssymTerm "a")) (conTerm 1 :: Term Integer)
                  @=? pevalLeNumTerm (conTerm 1 :: Term Integer) (pevalUMinusNumTerm $ ssymTerm "a"),
              testCase "On right constant Integers" $ do
                pevalLeNumTerm (ssymTerm "a") (conTerm 1 :: Term Integer)
                  @=? pevalLeNumTerm (conTerm $ -1 :: Term Integer) (pevalUMinusNumTerm $ ssymTerm "a"),
              testCase "On right constant left uminus Integers" $ do
                pevalLeNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (conTerm 1 :: Term Integer)
                  @=? pevalLeNumTerm (conTerm $ -1 :: Term Integer) (ssymTerm "a"),
              testCase "On left add concrete Integers" $ do
                pevalLeNumTerm (pevalAddNumTerm (conTerm 2) (ssymTerm "a")) (ssymTerm "b" :: Term Integer)
                  @=? pevalLeNumTerm (conTerm 2 :: Term Integer) (pevalAddNumTerm (ssymTerm "b") (pevalUMinusNumTerm $ ssymTerm "a")),
              testCase "On right add concrete Integers" $ do
                pevalLeNumTerm (ssymTerm "b" :: Term Integer) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? pevalLeNumTerm (conTerm $ -2 :: Term Integer) (pevalAddNumTerm (ssymTerm "a") (pevalUMinusNumTerm $ ssymTerm "b")),
              testCase "On left constant and right add concrete BVs should not be simplified" $ do
                pevalLeNumTerm (concSignedBV 1) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? leNumTerm (concSignedBV 1) (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                pevalLeNumTerm (concUnsignedBV 1) (pevalAddNumTerm (conTerm 2) (ssymTerm "a"))
                  @=? leNumTerm (concUnsignedBV 1) (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")),
              testCase "On right constant and left add concrete BVs should not be simplified" $ do
                pevalLeNumTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (conTerm 1)
                  @=? leNumTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (concSignedBV 1)
                pevalLeNumTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (conTerm 1)
                  @=? leNumTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (concUnsignedBV 1),
              testCase "On right constant BVs should not be simplified" $ do
                pevalLeNumTerm (ssymTerm "a") (concSignedBV 1)
                  @=? leNumTerm (ssymTerm "a" :: Term (IntN 5)) (concSignedBV 1)
                pevalLeNumTerm (ssymTerm "a") (concUnsignedBV 1)
                  @=? leNumTerm (ssymTerm "a" :: Term (WordN 5)) (concUnsignedBV 1),
              testCase "On right constant and left uminus BVs should not be simplified" $ do
                pevalLeNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (concSignedBV 1)
                  @=? leNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term (IntN 5)) (concSignedBV 1)
                pevalLeNumTerm (pevalUMinusNumTerm $ ssymTerm "a") (concUnsignedBV 1)
                  @=? leNumTerm (pevalUMinusNumTerm $ ssymTerm "a" :: Term (WordN 5)) (concUnsignedBV 1),
              testCase "On left add concrete BVs should not be simplified" $ do
                pevalLeNumTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (ssymTerm "b")
                  @=? leNumTerm (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a")) (ssymTerm "b" :: Term (IntN 5))
                pevalLeNumTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (ssymTerm "b")
                  @=? leNumTerm (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")) (ssymTerm "b" :: Term (WordN 5)),
              testCase "Lt on right add concrete BVs should not be simplified" $ do
                pevalLeNumTerm (ssymTerm "b") (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                  @=? leNumTerm
                    (ssymTerm "b" :: Term (IntN 5))
                    (pevalAddNumTerm (concSignedBV 2) (ssymTerm "a"))
                pevalLeNumTerm (ssymTerm "b") (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a"))
                  @=? leNumTerm
                    (ssymTerm "b" :: Term (WordN 5))
                    (pevalAddNumTerm (concUnsignedBV 2) (ssymTerm "a")),
              testCase "On symbolic" $ do
                pevalLeNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                  @=? leNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer)
            ],
      testCase "Gt should be delegated to Lt" $
        pevalGtNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
          @=? pevalLtNumTerm (ssymTerm "b" :: Term Integer) (ssymTerm "a"),
      testCase "Ge should be delegated to Le" $ do
        pevalGeNumTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
          @=? pevalLeNumTerm (ssymTerm "b" :: Term Integer) (ssymTerm "a")
    ]