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...

I don't see any error with the Z3 in your case. It gives a model that satisfies your formula. Btw, constant 0: (c[2]!0) #b0 and constant 1: (c[1]!1) #b1, are the evaluations that satisfy the exists part of your formula. Suggestion: Remove the eval and see if you still get 6 constants. — Tushar
Indeed, there is no error. This is not what I claim. In the model, the first constant is c[2]!0, which is actually the third constant in my vector "v". How can I know this without parsing the names of all constants of the model ? I need to understand how constants of the model are indexed. It would have been easier if I simply could evaluate v[i] in my model, but it does not evaluate correctly apparently. — Heyji
I think one key point is the fact that the only free variable in your formula is the function f. Rest of all (c[i] and x) are bound. For any free variable, you can just call model.eval. As an exercise, remove the exists quantifier from the second part of your formula, and then try eval. — Tushar
I changed s.add(exists(v[0],v[1],v[2],constraints)); by s.add(constraints); and it worked. +1 for your hint on eval only working on free variables. The eval method allows me to avoid understanding how constants of the model are indexed, which is still unclear at this stage. Thanks ! — Heyji

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2015-05-19T15:44:05

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.

Understanding the index of all constants of a model

1 Answers