Rename symbolic operators

CHANGELOG.md

@@ -47,6 +47,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - [Breaking] Moved `Grisette.Data.Class.Substitute` to `Grisette.Data.Class.SubstituteSym`. ([#146](https://github.com/lsrcz/grisette/pull/146))
 - [Breaking] Split the `Grisette.Data.Class.SafeArith` module to `Grisette.Data.Class.SafeDivision` and `Grisette.Data.Class.SafeLinearArith`. ([#146](https://github.com/lsrcz/grisette/pull/146))
 - [Breaking] Changed the API to `MonadFresh`. ([#156](https://github.com/lsrcz/grisette/pull/156))
+- [Breaking] Renamed multiple symbolic operators. ([#158](https://github.com/lsrcz/grisette/pull/158))
 
 ## [0.3.1.1] -- 2023-09-29
 

src/Grisette/Backend/SBV/Data/SMT/Solving.hs

@@ -64,7 +64,7 @@
 import Grisette.Core.Data.Class.ExtractSymbolics
   ( ExtractSymbolics (extractSymbolics),
   )
-import Grisette.Core.Data.Class.LogicalOp (LogicalOp (nots, (&&~)))
+import Grisette.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&)))
 import Grisette.Core.Data.Class.ModelOps
   ( ModelOps (exact, exceptFor),
     SymbolSetOps (isEmptySet),
@@ -214,9 +214,9 @@
 --
 -- >>> :set -XTypeApplications -XOverloadedStrings -XDataKinds
 -- >>> let a = "a" :: SymInteger
--- >>> solve (precise z3) $ a >~ 7 &&~ a <~ 9
+-- >>> solve (precise z3) $ a .> 7 .&& a .< 9
 -- Right (Model {a -> 8 :: Integer})
--- >>> solve (approx (Proxy @4) z3) $ a >~ 7 &&~ a <~ 9
+-- >>> solve (approx (Proxy @4) z3) $ a .> 7 .&& a .< 9
 -- Left Unsat
 --
 -- This may be avoided by setting an large enough reasoning precision to prevent
@@ -380,24 +380,24 @@
           [] -> return (cexes, Right previousModel)
           newInput : vs -> do
             let CEGISCondition nextPre nextPost = func newInput
-            let finalPre = pre &&~ nextPre
-            let finalPost = post &&~ nextPost
+            let finalPre = pre .&& nextPre
+            let finalPost = post .&& nextPost
             r <- go cexFormula newInput (newInput : inputs) finalPre finalPost
             case r of
               (newCexes, Left failure) -> return (cexes ++ newCexes, Left failure)
               (newCexes, Right mo) -> do
                 go1
-                  (cexFormula &&~ cexesAssertFun newCexes)
+                  (cexFormula .&& cexesAssertFun newCexes)
                   (cexes ++ newCexes)
                   mo
                   (newInput : inputs)
                   finalPre
                   finalPost
                   vs
       cexAssertFun input =
-        let CEGISCondition pre post = func input in pre &&~ post
+        let CEGISCondition pre post = func input in pre .&& post
       cexesAssertFun :: [inputs] -> SymBool
-      cexesAssertFun = foldl (\acc x -> acc &&~ cexAssertFun x) (con True)
+      cexesAssertFun = foldl (\acc x -> acc .&& cexAssertFun x) (con True)
       go ::
         SymBool ->
         inputs ->
@@ -407,7 +407,7 @@
         IO ([inputs], Either SolvingFailure PM.Model)
       go cexFormula inputs allInputs pre post =
         SBV.runSMTWith (sbvConfig config) $ do
-          let SymBool t = phi &&~ cexFormula
+          let SymBool t = phi .&& cexFormula
           (newm, a) <- lowerSinglePrim config t
           SBVC.query $
             applyTimeout config $
@@ -423,8 +423,8 @@
         where
           forallSymbols :: SymbolSet
           forallSymbols = extractSymbolics allInputs
-          phi = pre &&~ post
-          negphi = pre &&~ nots post
+          phi = pre .&& post
+          negphi = pre .&& symNot post
           check :: Model -> IO (Either SolvingFailure (inputs, PM.Model))
           check candidate = do
             let evaluated = evaluateSym False candidate negphi

src/Grisette/Core.hs

@@ -166,7 +166,7 @@ module Grisette.Core
     --
     -- >>> let a = "a" :: SymInteger
     -- >>> let b = "b" :: SymInteger
-    -- >>> a ==~ b
+    -- >>> a .== b
     -- (= a b)
 
     -- *** Creation of solvable type values
@@ -609,7 +609,7 @@ module Grisette.Core
     onUnion2,
     onUnion3,
     onUnion4,
-    (#~),
+    (.#),
 
     -- * Conversion between Concrete and Symbolic values
     ToCon (..),
@@ -842,9 +842,9 @@ module Grisette.Core
     -- >>> import Grisette.Backend.SBV
     -- >>> let x = "x" :: SymInteger
     -- >>> let y = "y" :: SymInteger
-    -- >>> solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 20)
+    -- >>> solve (precise z3) (x + y .== 6 .&& x - y .== 20)
     -- Right (Model {x -> 13 :: Integer, y -> -7 :: Integer})
-    -- >>> solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 19)
+    -- >>> solve (precise z3) (x + y .== 6 .&& x - y .== 19)
     -- Left Unsat
     --
     -- The first parameter of 'solve' is the solver configuration.
@@ -863,7 +863,7 @@ module Grisette.Core
     -- evaluate symbolic values. The following code evaluates the product of
     -- x and y under the solution of the equation system.
     --
-    -- >>> Right m <- solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 20)
+    -- >>> Right m <- solve (precise z3) (x + y .== 6 .&& x - y .== 20)
     -- >>> evaluateSym False m (x * y)
     -- -91
     --
@@ -921,7 +921,7 @@ module Grisette.Core
     --   res :: ExceptT Error UnionM ()
     --   res = do
     --     z <- x `sdiv` y
-    --     mrgIf (z >~ 0) (assert (x >=~ y)) (return ())
+    --     mrgIf (z .> 0) (assert (x .>= y)) (return ())
     -- :}
     --
     -- Then we can ask the solver to find a counter-example that would lead to
@@ -933,7 +933,7 @@ module Grisette.Core
     -- >>> res
     -- ExceptT {If (|| (= y 0) (&& (< 0 (div x y)) (! (<= y x)))) (If (= y 0) (Left Arith) (Left Assert)) (Right ())}
     --
-    -- > >>> solveExcept (UnboundedReasoning z3) (==~ Left Assert) res
+    -- > >>> solveExcept (UnboundedReasoning z3) (.== Left Assert) res
     -- > Right (Model {x -> -6 :: Integer, y -> -3 :: Integer}) -- possible output
     --
     -- Grisette also provide implementation for counter-example guided inductive
@@ -1050,7 +1050,7 @@ import Grisette.Core.Control.Monad.UnionM
     UnionM,
     liftToMonadUnion,
     unionSize,
-    (#~),
+    (.#),
   )
 import Grisette.Core.Data.Class.BitVector
   ( BV (..),

src/Grisette/Core/Control/Monad/CBMCExcept.hs

@@ -82,8 +82,8 @@ import Grisette.Core.Data.Class.Mergeable
     rootStrategy1,
     wrapStrategy,
   )
-import Grisette.Core.Data.Class.SEq (SEq ((==~)))
-import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (<=~), (<~), (>=~), (>~)))
+import Grisette.Core.Data.Class.SEq (SEq ((.==)))
+import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (.<), (.<=), (.>), (.>=)))
 import Grisette.Core.Data.Class.SimpleMergeable
   ( SimpleMergeable (mrgIte),
     SimpleMergeable1 (liftMrgIte),
@@ -351,8 +351,8 @@ instance (Monad m) => OrigExcept.MonadError e (CBMCExceptT e m) where
   {-# INLINE catchError #-}
 
 instance (SEq (m (CBMCEither e a))) => SEq (CBMCExceptT e m a) where
-  (CBMCExceptT a) ==~ (CBMCExceptT b) = a ==~ b
-  {-# INLINE (==~) #-}
+  (CBMCExceptT a) .== (CBMCExceptT b) = a .== b
+  {-# INLINE (.==) #-}
 
 instance (EvaluateSym (m (CBMCEither e a))) => EvaluateSym (CBMCExceptT e m a) where
   evaluateSym fillDefault model (CBMCExceptT v) = CBMCExceptT $ evaluateSym fillDefault model v
@@ -441,10 +441,10 @@ instance
   {-# INLINE unionIf #-}
 
 instance (SOrd (m (CBMCEither e a))) => SOrd (CBMCExceptT e m a) where
-  (CBMCExceptT l) <=~ (CBMCExceptT r) = l <=~ r
-  (CBMCExceptT l) <~ (CBMCExceptT r) = l <~ r
-  (CBMCExceptT l) >=~ (CBMCExceptT r) = l >=~ r
-  (CBMCExceptT l) >~ (CBMCExceptT r) = l >~ r
+  (CBMCExceptT l) .<= (CBMCExceptT r) = l .<= r
+  (CBMCExceptT l) .< (CBMCExceptT r) = l .< r
+  (CBMCExceptT l) .>= (CBMCExceptT r) = l .>= r
+  (CBMCExceptT l) .> (CBMCExceptT r) = l .> r
   symCompare (CBMCExceptT l) (CBMCExceptT r) = symCompare l r
 
 instance

src/Grisette/Core/Control/Monad/UnionM.hs

@@ -33,7 +33,7 @@ module Grisette.Core.Control.Monad.UnionM
     liftToMonadUnion,
     underlyingUnion,
     isMerged,
-    (#~),
+    (.#),
     IsConcrete,
     unionSize,
   )
@@ -64,16 +64,16 @@ import Grisette.Core.Data.Class.GPretty
   ( GPretty (gpretty),
     groupedEnclose,
   )
-import Grisette.Core.Data.Class.ITEOp (ITEOp (ites))
+import Grisette.Core.Data.Class.ITEOp (ITEOp (symIte))
 import Grisette.Core.Data.Class.LogicalOp
-  ( LogicalOp (implies, nots, xors, (&&~), (||~)),
+  ( LogicalOp (symImplies, symNot, symXor, (.&&), (.||)),
   )
 import Grisette.Core.Data.Class.Mergeable
   ( Mergeable (rootStrategy),
     Mergeable1 (liftRootStrategy),
     MergingStrategy (SimpleStrategy),
   )
-import Grisette.Core.Data.Class.SEq (SEq ((==~)))
+import Grisette.Core.Data.Class.SEq (SEq ((.==)))
 import Grisette.Core.Data.Class.SimpleMergeable
   ( SimpleMergeable (mrgIte),
     SimpleMergeable1 (liftMrgIte),
@@ -83,7 +83,7 @@ import Grisette.Core.Data.Class.SimpleMergeable
     mrgIf,
     mrgSingle,
     simpleMerge,
-    (#~),
+    (.#),
   )
 import Grisette.Core.Data.Class.Solvable
   ( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),
@@ -385,10 +385,10 @@ instance UnionLike UnionM where
   {-# INLINE unionIf #-}
 
 instance (SEq a) => SEq (UnionM a) where
-  x ==~ y = simpleMerge $ do
+  x .== y = simpleMerge $ do
     x1 <- x
     y1 <- y
-    mrgSingle $ x1 ==~ y1
+    mrgSingle $ x1 .== y1
 
 -- | Lift the 'UnionM' to any 'MonadUnion'.
 liftToMonadUnion :: (Mergeable a, MonadUnion u) => UnionM a -> u a
@@ -498,28 +498,28 @@ instance (Num a, Mergeable a) => Num (UnionM a) where
   signum x = x >>= mrgSingle . signum
 
 instance (ITEOp a, Mergeable a) => ITEOp (UnionM a) where
-  ites = mrgIf
+  symIte = mrgIf
 
 instance (LogicalOp a, Mergeable a) => LogicalOp (UnionM a) where
-  a ||~ b = do
+  a .|| b = do
     a1 <- a
     b1 <- b
-    mrgSingle $ a1 ||~ b1
-  a &&~ b = do
+    mrgSingle $ a1 .|| b1
+  a .&& b = do
     a1 <- a
     b1 <- b
-    mrgSingle $ a1 &&~ b1
-  nots x = do
+    mrgSingle $ a1 .&& b1
+  symNot x = do
     x1 <- x
-    mrgSingle $ nots x1
-  xors a b = do
+    mrgSingle $ symNot x1
+  symXor a b = do
     a1 <- a
     b1 <- b
-    mrgSingle $ a1 `xors` b1
-  implies a b = do
+    mrgSingle $ a1 `symXor` b1
+  symImplies a b = do
     a1 <- a
     b1 <- b
-    mrgSingle $ a1 `implies` b1
+    mrgSingle $ a1 `symImplies` b1
 
 instance (Solvable c t, Mergeable t) => Solvable c (UnionM t) where
   con = mrgSingle . con

src/Grisette/Core/Data/Class/CEGISSolver.hs

@@ -137,12 +137,12 @@ class
 -- CEGIS with a single symbolic input to represent a set of inputs.
 --
 -- The following example tries to find the value of @c@ such that for all
--- positive @x@, @x * c < 0 && c > -2@. The @c >~ -2@ clause is used to make
+-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make
 -- the solution unique.
 --
 -- >>> :set -XOverloadedStrings
 -- >>> let [x,c] = ["x","c"] :: [SymInteger]
--- >>> cegis (precise z3) x (cegisPrePost (x >~ 0) (x * c <~ 0 &&~ c >~ -2))
+-- >>> cegis (precise z3) x (cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2))
 -- ([],Right (Model {c -> -1 :: Integer}))
 cegis ::
   ( CEGISSolver config failure,
@@ -251,7 +251,7 @@ cegisExceptStdVCMultiInputs config cexes =
 -- readability and modularity of the code.
 --
 -- The following example tries to find the value of @c@ such that for all
--- positive @x@, @x * c < 0 && c > -2@. The @c >~ -2@ assertion is used to make
+-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ assertion is used to make
 -- the solution unique.
 --
 -- >>> :set -XOverloadedStrings
@@ -260,9 +260,9 @@ cegisExceptStdVCMultiInputs config cexes =
 -- >>> :{
 --   res :: ExceptT VerificationConditions UnionM ()
 --   res = do
---     symAssume $ x >~ 0
---     symAssert $ x * c <~ 0
---     symAssert $ c >~ -2
+--     symAssume $ x .> 0
+--     symAssert $ x * c .< 0
+--     symAssert $ c .> -2
 -- :}
 --
 -- >>> :{
@@ -327,7 +327,7 @@ cegisExceptVC config inputs f v =
 -- The '()' result will not fail any conditions.
 --
 -- The following example tries to find the value of @c@ such that for all
--- positive @x@, @x * c < 0 && c > -2@. The @c >~ -2@ assertion is used to make
+-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ assertion is used to make
 -- the solution unique.
 --
 -- >>> :set -XOverloadedStrings
@@ -336,9 +336,9 @@ cegisExceptVC config inputs f v =
 -- >>> :{
 --   res :: ExceptT VerificationConditions UnionM ()
 --   res = do
---     symAssume $ x >~ 0
---     symAssert $ x * c <~ 0
---     symAssert $ c >~ -2
+--     symAssume $ x .> 0
+--     symAssert $ x * c .< 0
+--     symAssert $ c .> -2
 -- :}
 --
 -- >>> cegisExceptStdVC (precise z3) x res

src/Grisette/Core/Data/Class/ITEOp.hs

@@ -50,31 +50,31 @@ import Grisette.IR.SymPrim.Data.SymPrim
 -- >>> let a = "a" :: SymBool
 -- >>> let b = "b" :: SymBool
 -- >>> let c = "c" :: SymBool
--- >>> ites a b c
+-- >>> symIte a b c
 -- (ite a b c)
 class ITEOp v where
-  ites :: SymBool -> v -> v -> v
+  symIte :: SymBool -> v -> v -> v
 
 -- ITEOp instances
 #define ITEOP_SIMPLE(type) \
 instance ITEOp type where \
-  ites (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \
-  {-# INLINE ites #-}
+  symIte (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \
+  {-# INLINE symIte #-}
 
 #define ITEOP_BV(type) \
 instance (KnownNat n, 1 <= n) => ITEOp (type n) where \
-  ites (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \
-  {-# INLINE ites #-}
+  symIte (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \
+  {-# INLINE symIte #-}
 
 #define ITEOP_BV_SOME(symtype, bf) \
 instance ITEOp symtype where \
-  ites c = bf (ites c) "ites"; \
-  {-# INLINE ites #-}
+  symIte c = bf (symIte c) "symIte"; \
+  {-# INLINE symIte #-}
 
 #define ITEOP_FUN(op, cons) \
 instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa op sb) where \
-  ites (SymBool c) (cons t) (cons f) = cons $ pevalITETerm c t f; \
-  {-# INLINE ites #-}
+  symIte (SymBool c) (cons t) (cons f) = cons $ pevalITETerm c t f; \
+  {-# INLINE symIte #-}
 
 #if 1
 ITEOP_SIMPLE(SymBool)