该matplotlib.pyplot.contour()函数需要3个输入数组X,Y和Z.
数组X并Y指定点的x坐标和y坐标,同时Z指定在点处评估的感兴趣函数的对应值.
据我所知,np.meshgrid()可以很容易地生成作为参数的数组contour():
X = np.arange(0,5,0.01)
Y = np.arange(0,3,0.01)
X_grid, Y_grid = np.meshgrid(X,Y)
Z_grid = X_grid**2 + Y_grid**2
plt.contour(X_grid, Y_grid, Z_grid) # Works fine
这很好用.方便的是,这也很好:
plt.contour(X, Y, Z_grid) # Works fine too
但是,为什么Z输入需要是2D阵列？
为什么类似以下内容不允许,即使它指定所有相同的数据对齐？
plt.contour(X_grid.ravel(), Y_grid.ravel(), Z_grid.ravel()) # Disallowed
另外,只 Z指定了什么是语义(没有相应的X和Y)？
我正在使用Z3 SMT求解器来解决我在逻辑QF_BV中使用SMTLIB 2语言表达的问题.
该模型是不可满足的,我试图让求解器产生一个不满足的核心.
我的模型由几个"强制"约束组成,我使用assert语句指定.
我想要使用(assert (! (EXPR) :named NAME))构造来指定我想要用于不良核心生成的断言.
unsat正如预期的那样,Z3给了我一个.然而,Z3似乎总是抛弃一个由所有命名的断言组成的"琐碎的"不饱和核心.
我知道我的命名断言中存在一个子集,这是一个不可靠的核心.我使用Yices SMT求解器找到了这个核心,它经常给我相对较小的不饱和核心.Yices模型与Z3模型相同(几乎是从SMT2到Yices输入语言的逐行转换).
产生"好"的不良核心是解决者特有的功能,还是我可以做出任何通用的建议/改变来帮助Z3给我一个更好的核心？
我试图使用大括号来定义字符串{ },而不是双引号的" ",所以我没有逃避几个字符(如$,[,]).
但是,当我的字符串需要在其中包含单个字符串时,我遇到了一些问题{.
我知道我可以通过简单地使用双引号字符串来实现这一点{,但是如何使用"花括号字符串"来实现它？
例如.我想要puts以下字符串' proc foo {} { '到stdout.
puts "proc foo \{ \} \{"给了我想要的输出:' proc foo {} { '
然而,puts { proc foo \{ \} \{ }给我:' proc foo\{\}\{ '通过字面打印反斜杠.
如果我跳过反斜杠,puts { proc foo { } {它会抱怨缺少支撑.
此外,如果所需的字符串中有匹配的闭括号,它可以正常工作.
puts { proc foo { } { } }给了我预期的:' proc foo {} {} '
在"花括号"字符串中逃避单个不匹配的花括号的正确方法是什么？