Understanding the index of all constants of a model

Question

I guess my issue is linked with Read func interp of a z3 array from the z3 model, but still I can't understand how to fix it.

Edit: I think it is also linked with de bruijn index: Understanding the indexing of bound variables in Z3

Here is the small example I have built to explain the problem:

#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;
}

By runing this program, I get the following output:

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

I don't get:

• Why it enumerates 6 constants and not 3 ?
• How to retrieve the value of the nth constant of vector "v" without parsing their name, which is not the nth constant of the model "m" ?
• Why c[1] evaluates to 0 while I would have expected it to evaluate to 1 ?
• What "!x" means in the name of the constant c[2]!0 and c[1]!1 ?

I would like to re-inject evaluations of c[0], c[1] and c[2] into the function f() in order to simplify its expression (I expect to get x+1)

Note: c[0] is not used on purpose...

Answer 1

Thanks Tushar for answering the post. You are right that the additional variables come from the existential quantifier. Z3 will skolemize these variables and as it currently stands, the model returned by Z3 includes constants from skolemized existential quantifiers. This is evidently confusing and we may in the future filter such variables (and functions) away from the model construction. On the other hand, the naming conventions used for the existential variables retain the names from the quantifiers so that it may be possible, at least manually, to track back the origin of those extra variables.