Commits

Nathan Howell  committed f1779f9

Support distinct predicate

  • Participants
  • Parent commits cabe346

Comments (1)

  1. Iago Abal

    For some reason we forgot to include distinct... we'll accept this changeset, but fixing how it was implemented. Distinct is not a BoolMultiOp, a BoolOp is supposed to have boolean arguments, while distinct works for any scalar type.

    By the way, next time follow our "documentation style" when adding new foreign imports do Z3/Base/C.hsc.

Files changed (5)

     , mkXor
     , mkAnd
     , mkOr
+    , mkDistinct
     , mkAdd
     , mkMul
     , mkSub
       AST <$> z3_mk_or cptr n (castPtr aptr)
   where n = fromIntegral $ length es
 
+mkDistinct :: Context -> [AST Bool] -> IO (AST Bool)
+mkDistinct _ [] = error "Z3.Base.mkDistinct: empty list of expressions"
+mkDistinct c es =
+  withArray es $ \aptr ->
+    withContext c $ \cptr ->
+      AST <$> z3_mk_distinct cptr n (castPtr aptr)
+  where n = fromIntegral $ length es
+
 -- | Create an AST node representing args[0] + ... + args[num_args-1].
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>

File Z3/Base/C.hsc

     z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
 
 -- TODO: Z3_mk_distinct
+foreign import ccall unsafe "Z3_mk_distinct"
+    z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
 
 -- | Create an AST node representing not(a).
 --

File Z3/Lang/Exprs.hs

     deriving (Eq,Show)
 
 -- | Boolean variadic operations.
-data BoolMultiOp = And | Or
+data BoolMultiOp = And | Or | Distinct
     deriving (Eq,Show)
 
 -- | Commutative ring operations.

File Z3/Lang/Monad.hs

 mkBoolBin Iff     = liftZ3Op3 Base.mkIff
 
 mkBoolMulti :: BoolMultiOp -> [Base.AST Bool] -> Z3 (Base.AST Bool)
-mkBoolMulti And = liftZ3Op2 Base.mkAnd
-mkBoolMulti Or  = liftZ3Op2 Base.mkOr
+mkBoolMulti And      = liftZ3Op2 Base.mkAnd
+mkBoolMulti Or       = liftZ3Op2 Base.mkOr
+mkBoolMulti Distinct = liftZ3Op2 Base.mkDistinct
 
 mkPattern :: Base.Z3Type a => [Base.AST a] -> Z3 Base.Pattern
 mkPattern = liftZ3Op2 Base.mkPattern

File Z3/Lang/Prelude.hs

     , not_
     , and_, (&&*)
     , or_, (||*)
+    , distinct_
     , xor
     , implies, (==>)
     , iff, (<=>)
 or_ :: [Expr Bool] -> Expr Bool
 or_ [] = false
 or_ bs = BoolMulti Or bs
+-- | Boolean variadic /distinct/.
+distinct_ :: [Expr Bool] -> Expr Bool
+distinct_ [] = true
+distinct_ bs = BoolMulti Distinct bs
 
 -- | Boolean binary /and/.
 --