小编S.N*_*.N.的帖子

.net API具有以下Context的构造函数:

Context (Dictionary< string, string > settings)

如何获取所有可能设置的列表？

具体来说,我感兴趣的是如何让Z3生产不饱和核心,即相当于SMT lib产生的不饱和核心.

这是一个由三部分组成的问题，涉及 Z3 (Z3Py) 的 Python API 的使用。

1. 我以为我知道常量和变量之间的区别，但显然不知道。我想我可以声明一种排序并实例化该排序的变量，如下所示：

   Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
   n1 = Node('n1') # c.f. x = Int('x')
   

   Run Code Online (Sandbox Code Playgroud)

   但是 python 抛出一个异常，说你不能“调用 Node”。似乎唯一有效的是声明n1一个常量

   Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
   n1 = Const('n1',Node)
   

   Run Code Online (Sandbox Code Playgroud)

   但我对此感到困惑，因为我认为 a1,a2,a3 是常数。也许 n1 是一个符号常量，但我如何声明一个实际变量？

2. 如何创建常量集？我尝试从一个空集开始并添加到其中，但这不起作用

   Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
   n1 = Const('n1',Node)
   nodes = EmptySet(Node)
   SetAdd(nodes, a1) #<-- want to create a set {a1}
   solve([IsMember(n1,nodes)])
   

   Run Code Online (Sandbox Code Playgroud)

   但这不起作用 Z3 没有返回任何解决方案。另一方面，将第三行替换为

   nodes = Const('nodes',SetSort(Node))
   

   Run Code Online (Sandbox Code Playgroud)

   现在过于宽松，允许 Z3 将节点解释为满足公式所需的任何节点集。如何只创建集合 {a1}？

3. 除了看起来有点麻烦的数据类型声明之外，是否有一种简单的方法来创建对？例如

   Edge = Datatype('Edge')
   Edge.declare('pr', ('fst', Node), ('snd',Node)) …

   Run Code Online (Sandbox Code Playgroud)

我尝试在F#中定义我自己的逻辑隐含运算符,如下所示

let (-->) p q = (not p) || q

但是当我真正试用它时,似乎没有实现短路OR

> false --> ((2/0)=1);;
System.DivideByZeroException: Attempted to divide by zero.at <StartupCode$FSI_0015>.$FSI_0015.main@()
Stopped due to error
> 

它不应该评估结果,但它是

有谁能看到这里有什么问题？我在VS 2012中运行F#