了解模型所有常量的索引

Question

我想我的问题与 Read func interp of a z3 array from the z3 model 有关，但我仍然不明白如何解决它。

编辑：我认为它也与 de bruijn 索引相关联：Understanding the indexing of bound variables in Z3

这是我为解释问题而构建的小示例：

#include <iostream>
#include <sstream>
#include <cassert>
#include "z3++.h"

using namespace z3;

int main(void)
{
    context ctx;
    params p(ctx);
    p.set("MACRO_FINDER",true);

    expr_vector v(ctx);
    sort_vector sv(ctx);
    for(int i = 0; i < 3; i++)
    {
        std::ostringstream o;
        o << "c[" << i << "]";
        expr c = ctx.bv_const(o.str().c_str(),1);
        v.push_back(c);
        sv.push_back(ctx.bv_sort(1));
    }

    expr x = ctx.bv_const("x",8);

    v.push_back(x);
    sv.push_back(ctx.bv_sort(8));

    expr one_bit = ctx.bv_val(1,1);
    expr two = ctx.bv_val(2,8);
    expr one = ctx.bv_val(1,8);
    expr zero = ctx.bv_val(0,8);
    expr fcore = x + ite(v[1] == one_bit , one, zero) + ite(v[2] == one_bit, two, zero); 

    func_decl f = ctx.function("f",sv,ctx.bv_sort(8));

    solver s(ctx);
    s.set(p);
    s.add(forall(v,f(v) == fcore));

    expr_vector t1(ctx);
    expr_vector t2(ctx);
    t1.push_back(v[0]); t1.push_back(v[1]); t1.push_back(v[2]); t1.push_back(ctx.bv_val(0,8));
    t2.push_back(v[0]); t2.push_back(v[1]); t2.push_back(v[2]); t2.push_back(ctx.bv_val(1,8));
    expr constraints = (f(t1) == ctx.bv_val(1,8)) && (f(t2) == ctx.bv_val(2,8));

    s.add(exists(v[0],v[1],v[2],constraints));

    std::cout << "Solver: " << s << "\n\n";
    if(s.check()==sat)
    {
        model m = s.get_model();
        std::cout << "Model: " << m << "\n\n";
        std::cout << "Number of constants: " << m.num_consts() << "\n";

        expr F = m.eval(f(v),true);

        for(size_t i = 0; i < m.num_consts(); ++i)
            std::cout << "\t constant " << i << ": " << "(" << m.get_const_decl(i).name() << ") " << m.get_const_interp(m.get_const_decl(i)) << "\n";

        std::cout << "Number of functions: " << m.num_funcs() << "\n";
        std::cout << "\t" << F << "\n";
    }
    else
        std::cout << "unsat\n";
    return 0;
}

通过运行这个程序，我得到以下输出：

Solver: (solver
  (forall ((|c[0]| (_ BitVec 1))
           (|c[1]| (_ BitVec 1))
           (|c[2]| (_ BitVec 1))
           (x (_ BitVec 8)))
    (= (f |c[0]| |c[1]| |c[2]| x)
       (bvadd x (ite (= |c[1]| #b1) #x01 #x00) (ite (= |c[2]| #b1) #x02 #x00))))
  (exists ((|c[0]| (_ BitVec 1)) (|c[1]| (_ BitVec 1)) (|c[2]| (_ BitVec 1)))
    (and (= (f |c[0]| |c[1]| |c[2]| #x00) #x01)
         (= (f |c[0]| |c[1]| |c[2]| #x01) #x02))))

Model: (define-fun |c[2]!0| () (_ BitVec 1)
  #b0)
(define-fun |c[1]!1| () (_ BitVec 1)
  #b1)
(define-fun f ((x!1 (_ BitVec 1))
 (x!2 (_ BitVec 1))
 (x!3 (_ BitVec 1))
 (x!4 (_ BitVec 8))) (_ BitVec 8)
  (bvadd x!4 (ite (= #b1 x!3) #x02 #x00) (ite (= #b1 x!2) #x01 #x00)))

Number of constants: 2
         constant 0: (c[2]!0) #b0
         constant 1: (c[1]!1) #b1
         constant 2: (c[0]) #b0
         constant 3: (c[1]) #b0
         constant 4: (c[2]) #b0
         constant 5: (x) #x00
Number of functions: 1
        #x00

我不明白：

为什么它枚举了 6 个常量而不是 3 个？
如何在不解析其名称的情况下检索向量 "v" 的第 n 个常量的值，这不是模型 "m" 的第 n 个常量？
为什么 c[1] 的计算结果为 0 而我期望它的计算结果为 1？
“!x”在常量 c[2]!0 和 c[1]!1 中的含义是什么？

我想将 c[0]、c[1] 和 c[2] 的求值重新注入函数 f() 以简化其表达式（我希望得到 x+1）

注意：c[0] 不是有意使用的...

Answer 1

感谢 Tushar 回答 post。你是对的，附加变量来自存在量词。 Z3 将对这些变量进行 skolemized，就目前而言，Z3 返回的模型包括来自 skolemized 存在量词的常量。这显然令人困惑，我们将来可能会过滤这些变量（和函数）远离模型构建。另一方面，用于存在变量的命名约定保留了量词的名称，因此至少可以手动追溯这些额外变量的来源。

了解模型所有常量的索引

Understanding the index of all constants of a model

z3