如何计算api中smtlib2文件的总约束数

Question

我使用Z3_ast fs = Z3_parse_smtlib2_file(ctx,arg[1],0,0,0,0,0,0)来读取文件。

另外添加到使用的解算器expr F = to_expr(ctx,fs)然后s.add(F)。

我的问题是如何获得每个实例中总约束的数量？

我也尝试了F.num_args()，但是，它在某些情况下给出错误的大小。

是否有任何方法来计算总约束？

Answer 1

在向某个目标添加F后，使用Goal.size()可能会做你想做的。下面是Python API中描述的链接，我敢肯定，你可以找到C/C++ API中的等价物：http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#Goal-size

的expr F代表抽象语法树，所以F.num_args()返回（一步）的儿童人数F有，这可能是为什么你一直在尝试并不总是工作。例如，假设F = a + b，然后F.num_args() = 2。而且，如果F = a + b*c，那么F.num_args() = 2以及那里的子女将是a和b*c（假定通常的操作顺序）。因此，要计算约束的数量（如果您的定义不同于Goal.size()产生的结果），则可以使用遍历树的递归方法。

我已经包括一个例子，突出显示所有这些（z3py链接在这里：http://rise4fun.com/Z3Py/It5E）。例如，我对约束的定义（或者某种意义上的表达的复杂性）可能是叶子的数量或表达的深度。您可以根据需要获得详细的信息，例如，计算不同类型的操作数以适应您的约束定义，因为您的问题并不完全清楚。例如，您可以将约束定义为表达式中出现的等式和/或不等式的数量。这可能需要进行修改才能用于具有量词，数组或未解释函数的公式。另请注意，Z3可能会自动将事情简化（例如，1 - 1在以下示例中简化为0）。

a, b, c = Reals('a b c') 

F = a + b 
print F.num_args() # 2 

F = a + b * c 
print F.num_args() # 2 

print F.children() # [a,b*c] 

g = Goal() 
g.add(F == 0) 
print g.size() # number of constraints = 1 

g.add(Or(F == 0, F == 1, F == 2, F == 3)) 
print g.size() # number of constraints = 2 
print g 

g.add(And(F == 0, F == 1, F == 2, F == 3)) 
print g.size() # number of constraints = 6 
print g 

def count_constraints(c,d,f): 
    print 'depth: ' + str(d) + ' expr: ' + str(f) 
    if f.num_args() == 0: 
    return c + 1 
    else: 
    d += 1 
    for a in f.children(): 
     c += count_constraints(0, d, a) 
    return c 

exp = a + b * c + a + c * c 
print count_constraints(0,0,exp) 

exp = And(a == b, b == c, a == 0, c == 0, b == 1 - 1) 
print count_constraints(0,0,exp) 

q, r, s = Bools('q r s') 
exp = And(q, r, s) 
print count_constraints(0,0,exp)