Permalink
Browse files

Add some modulo-arithmetic related functions. Experimental.

Things gets slow quickly.
  • Loading branch information...
1 parent 06dd060 commit 113f9526e4fe199d002e00ce7fb097d643b31547 @yav committed Apr 27, 2009
Showing with 31 additions and 0 deletions.
  1. +1 −0 presburger.cabal
  2. +30 −0 src/Data/Integer/Presburger/ModArith.hs
View
@@ -20,6 +20,7 @@ Exposed-modules:
Data.Integer.Presburger.SolveDiv
Data.Integer.Presburger.Notation
Data.Integer.Presburger.HOAS
+ Data.Integer.Presburger.ModArith
Data.Integer.Presburger.Utils
Extensions:
@@ -0,0 +1,30 @@
+module Data.Integer.Presburger.ModArith where
+
+import Data.Integer.Presburger
+
+is_nat :: Term -> Formula
+is_nat t = 0 :<=: t
+
+is_reminder :: Integer -> Term -> Formula
+is_reminder d r = is_nat r :/\: r :<: fromIntegral d
+
+-- | divMod t d == (q,r)
+div_mod_is :: Term -> Integer -> Term -> Term -> Formula
+div_mod_is t d q r = is_reminder d r :/\: d .* q + r :=: t
+
+-- | mod t d == r
+mod_is :: Term -> Integer -> Term -> Formula
+mod_is t d r = is_reminder d r :/\: d :| (t - r)
+
+bin_op_mod :: Integer -> (Term -> Term -> Term)
+ -> Term -> Term -> Term -> Formula
+bin_op_mod d f t1 t2 t3 = mod_is (f t1 t2) d t3
+
+add_mod, sub_mod, mul_mod :: Integer -> Term -> Term -> Term -> Formula
+add_mod d = bin_op_mod d (+)
+sub_mod d = bin_op_mod d (-)
+mul_mod d = bin_op_mod d (*)
+
+
+
+

0 comments on commit 113f952

Please sign in to comment.