Commits

Nathan Howell committed f8d8b1f

Support creating variables with a user specified name

  • Participants
  • Parent commits b3482cf

Comments (0)

Files changed (1)

Z3/Lang/Prelude.hs

 
     -- ** Commands
     , var
+    , namedVar
     , fun1, fun2, fun3, fun4, fun5
     , assert
     , let_
 ---------------------------------------------------------------------
 -- Commands
 
--- | Declare skolem variables.
---
-var :: forall a. IsTy a => Z3 (Expr a)
-var = do
-    (u, str) <- fresh
+createVar :: forall a. IsTy a => Int -> String -> Z3 (Expr a)
+createVar u str = do
     smb <- mkStringSymbol str
     (srt :: Base.Sort (TypeZ3 a)) <- mkSort
     cnst <- mkConst smb srt
     assert $ typeInv e
     return e
 
+-- | Declare skolem variables.
+--
+var :: IsTy a => Z3 (Expr a)
+var = do
+    (u, str) <- fresh
+    createVar u str
+
+-- | Declare skolem variables with a user specified name.
+--
+namedVar :: IsTy a => String -> Z3 (Expr a)
+namedVar name = do
+    (u, str) <- fresh
+    createVar u $ name ++ "/" ++ str
+
 -- | Declare uninterpreted function of arity 1.
 --
 fun1 :: (IsTy a, IsTy b) => Z3 (Expr a -> Expr b)