我尝试在Python中导入NumPy,但它没有成功:

>>> import numpy as np
    x=np.array([[7,8,5],[3,5,7]],np.int32)

   Traceback (most recent call last):
   File "<pyshell#3>", line 1, in <module>
   import numpy as np
   File "C:\Python27\lib\numpy\__init__.py", line 127, in <module>
   raise ImportError(msg)
   ImportError: Error importing numpy: you should not try to import numpy from
   its source directory; please exit the numpy source tree, and relaunch
   your Python interpreter from there.

我怎样才能解决这个问题？

有些人可以帮我看看如何在python中找到代码需要多少时间和内存？

以下脚本http://rise4fun.com/Z3Py/Cbl有什么问题？添加最后两行给出了以下错误'instancemethod' object is not #subscriptable

x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next')
location,location_next=Bools('location location_next')
x=0
location=BoolVal(False)
k=20
for i in range(k):
 s=Solver()
 s.add(Or(And(x_next-x>=2*t,x_next-x<=3*t,x_next<=12,t>0,Not(location)),
         And(x_next-x>=-2*t,x_next-x<=-t,x_next>=0,t>0,location)),location_next==If(And(Not(location),x_next>=12),True,If(And(location,x_next<=0),False,location)))

print s.check()
print s.model()
m=s.model
#x=m[x_next]
#location=m[location_next]

有人可以帮我指出使用一阶公式的下列方程的最佳编码,以便将其作为SMT求解器的输入吗？

x`=Ax+b

我已经安装了 python 和 Z3 并设置了 PYTHONPATH 与 Z3 python 目录的路径。

我通过运行 from z3 import * 导入 Z3

但在此之后，我收到一条持续的长错误消息，其以以下方式结束：

File "C:\Program Files\Microsoft Research\Z3-4.1\python\z3core.py", line 34, in init
    _lib = ctypes.CDLL(PATH)
  File "C:\Python27\lib\ctypes\__init__.py", line 365, in __init__
    self._handle = _dlopen(self._name, mode)
WindowsError: [Error 126] The specified module could not be found

有趣的是，一切都正常，直到我重新安装了 python 和 Z3。