From a37fd146b0dbb68c54223c1d828b33a35121d17f Mon Sep 17 00:00:00 2001
From: "ThanhVu (Vu) Nguyen" <tnguyen@cs.unm.edu>
Date: Sun, 2 Dec 2012 23:41:31 -0500
Subject: [PATCH] added is_expr_var and is_expr_val to check if a given
 expression is a value or a variable

---
 src/api/python/z3util.py | 56 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)
 create mode 100644 src/api/python/z3util.py

diff --git a/src/api/python/z3util.py b/src/api/python/z3util.py
new file mode 100644
index 000000000..402d29174
--- /dev/null
+++ b/src/api/python/z3util.py
@@ -0,0 +1,56 @@
+"""
+In Z3, variables are caleld *uninterpreted* consts and 
+variables are *interpreted* consts.
+"""
+
+def is_expr_var(v):
+    """
+    EXAMPLES:
+
+    >>> is_expr_var(Int('7'))
+    True
+    >>> is_expr_var(IntVal('7'))
+    False
+    >>> is_expr_var(Bool('y'))
+    True
+    >>> is_expr_var(Int('x') + 7 == Int('y'))
+    False
+    >>> LOnOff, (On,Off) = EnumSort("LOnOff",['On','Off'])
+    >>> Block,Reset,SafetyInjection=Consts("Block Reset SafetyInjection",LOnOff)
+    >>> is_expr_var(LOnOff)
+    False
+    >>> is_expr_var(On)
+    False
+    >>> is_expr_var(Block)
+    True
+    >>> is_expr_var(SafetyInjection)
+    True
+    """
+
+    return is_const(v) and v.decl().kind()==Z3_OP_UNINTERPRETED
+
+def is_expr_val(v):
+    """
+    EXAMPLES:
+
+    >>> is_expr_val(Int('7'))
+    False
+    >>> is_expr_val(IntVal('7'))
+    True
+    >>> is_expr_val(Bool('y'))
+    False
+    >>> is_expr_val(Int('x') + 7 == Int('y'))
+    False
+    >>> LOnOff, (On,Off) = EnumSort("LOnOff",['On','Off'])
+    >>> Block,Reset,SafetyInjection=Consts("Block Reset SafetyInjection",LOnOff)
+    >>> is_expr_val(LOnOff)
+    False
+    >>> is_expr_val(On)
+    True
+    >>> is_expr_val(Block)
+    False
+    >>> is_expr_val(SafetyInjection)
+    False
+    """        
+    return is_const(v) and v.decl().kind()!=Z3_OP_UNINTERPRETED
+