Add equality modulo an integer and negation normal form to formulas

src/Parser/PP.hs

@@ -30,10 +30,10 @@ languageDef =
                  Token.identStart      = letter <|> char '_',
                  Token.identLetter     = alphaNum <|> char '_',
                  Token.reservedNames   = ["true", "false", "EXISTS", "FORALL"],
-                 Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
+                 Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", "=%", "!=%",
                                           "+", "-", "*", "&&", "||", "!", ":"]
                  }
- 
+
 lexer :: Token.TokenParser ()
 lexer = Token.makeTokenParser languageDef
 
@@ -103,7 +103,8 @@ parseOp = (reservedOp "<" *> return Lt) <|>
           (reservedOp "=" *> return Eq) <|>
           (reservedOp "!=" *> return Ne) <|>
           (reservedOp ">" *> return Gt) <|>
-          (reservedOp ">=" *> return Ge)
+          (reservedOp "=%" *> (ModEq <$> integer)) <|>
+          (reservedOp "!=%" *> (ModNe <$> integer))
 
 linIneq :: Parser (Formula String)
 linIneq = do

src/Property.hs

@@ -47,7 +47,7 @@ instance Functor Term where
         fmap f (t :/: u) = fmap f t :/: fmap f u
         fmap f (t :%: u) = fmap f t :%: fmap f u
 
-data Op = Gt | Ge | Eq | Ne | Le | Lt deriving (Eq)
+data Op = Gt | Ge | Eq | Ne | Le | Lt | ModEq Integer | ModNe Integer deriving (Eq)
 
 instance Show Op where
         show Gt = ">"
@@ -56,6 +56,18 @@ instance Show Op where
         show Ne = "≠"
         show Le = "≤"
         show Lt = "<"
+        show (ModEq m) = "≡_" ++ show m
+        show (ModNe m) = "≢_" ++ show m
+
+negateOp :: Op -> Op
+negateOp Gt = Le
+negateOp Ge = Lt
+negateOp Eq = Ne
+negateOp Ne = Eq
+negateOp Le = Gt
+negateOp Lt = Ge
+negateOp (ModEq m) = (ModNe m)
+negateOp (ModNe m) = (ModEq m)
 
 data QuantFormula a = ExQuantFormula [a] (Formula a)
              deriving (Eq)
@@ -71,6 +83,14 @@ data Formula a =
 infixr 3 :&:
 infixr 2 :|:
 
+negationNormalForm :: Formula a -> Formula a
+negationNormalForm (Neg (FTrue)) = FFalse
+negationNormalForm (Neg (FFalse)) = FTrue
+negationNormalForm (Neg (g :&: h)) = (negationNormalForm (Neg g)) :|: (negationNormalForm (Neg h))
+negationNormalForm (Neg (g :|: h)) = (negationNormalForm (Neg g)) :&: (negationNormalForm (Neg h))
+negationNormalForm (Neg (LinearInequation u op t)) = LinearInequation u (negateOp op) t
+negationNormalForm f = f
+
 quantifiedVariables :: QuantFormula a -> [a]
 quantifiedVariables (ExQuantFormula xs _) = xs