Allow usage of division and modulus in predicate terms

examples/remainder_m3_c1.pp

@@ -112,10 +112,10 @@
         "_mod1",
         "_mod2"
     ],
-    "predicate": "EXISTS k : 0 * _mod0 + 1 * _mod1 + 2 * _mod2 = 1 + 3 * k",
+    "predicate": "( 0 * _mod0 + 1 * _mod1 + 2 * _mod2 ) % 3 = 1",
     "trueStates": [
         "_mod1",
         "_modpassivetrue"
     ],
     "title": "Modulo Protocol with m = 3 and c = 1"
-}
\ No newline at end of file
+}

src/Parser/PP.hs

@@ -84,7 +84,7 @@ prefix name fun = Prefix ( reservedOp name *> return fun )
 termOperatorTable :: [[Operator String () Identity (Term String)]]
 termOperatorTable =
         [ [ prefix "-" Minus ]
-        , [ binary "*" (:*:) AssocLeft ]
+        , [ binary "*" (:*:) AssocLeft, binary "/" (:/:) AssocLeft, binary "%" (:%:) AssocLeft ]
         , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
         ]
 

src/Property.hs

@@ -23,6 +23,8 @@ data Term a =
         | Term a :+: Term a
         | Term a :-: Term a
         | Term a :*: Term a
+        | Term a :/: Term a -- integer division truncated toward negative infinity
+        | Term a :%: Term a -- integer modulos, satisfying (x / y)*y + (x % y) = x
         deriving (Eq)
 
 instance (Show a) => Show (Term a) where
@@ -32,6 +34,8 @@ instance (Show a) => Show (Term a) where
         show (t :+: u) = "(" ++ show t ++ " + " ++ show u ++ ")"
         show (t :-: u) = "(" ++ show t ++ " - " ++ show u ++ ")"
         show (t :*: u) = show t ++ " * " ++ show u
+        show (t :/: u) = show t ++ " / " ++ show u
+        show (t :%: u) = show t ++ " % " ++ show u
 
 instance Functor Term where
         fmap f (Var x) = Var (f x)
@@ -40,6 +44,8 @@ instance Functor Term where
         fmap f (t :+: u) = fmap f t :+: fmap f u
         fmap f (t :-: u) = fmap f t :-: fmap f u
         fmap f (t :*: u) = fmap f t :*: fmap f u
+        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)
 

src/Solver/Formula.hs

@@ -15,6 +15,8 @@ evaluateTerm (Minus t) m = - evaluateTerm t m
 evaluateTerm (t :+: u) m = evaluateTerm t m + evaluateTerm u m
 evaluateTerm (t :-: u) m = evaluateTerm t m - evaluateTerm u m
 evaluateTerm (t :*: u) m = evaluateTerm t m * evaluateTerm u m
+evaluateTerm (t :/: u) m = (evaluateTerm t m) `sDiv` (evaluateTerm u m)
+evaluateTerm (t :%: u) m = (evaluateTerm t m) `sMod` (evaluateTerm u m)
 
 opToFunction :: Op -> SInteger -> SInteger -> SBool
 opToFunction Gt = (.>)