z3 - Understanding the index of all constants of a model -

i guess issue linked read func interp of z3 array z3 model, still can't understand how fix it.

edit: think linked de bruijn index: understanding indexing of bound variables in z3

here small example have built explain 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 = 0; < 3; i++)     {         std::ostringstream o;         o << "c[" << << "]";         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 2 = ctx.bv_val(2,8);     expr 1 = ctx.bv_val(1,8);     expr 0 = 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 = 0; < m.num_consts(); ++i)             std::cout << "\t constant " << << ": " << "(" << 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 program, 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 enumerates 6 constants , not 3 ?
• how retrieve value of nth constant of vector "v" without parsing name, not nth constant of model "m" ?
• why c[1] evaluates 0 while have expected evaluate 1 ?
• what "!x" means in name of constant c[2]!0 , c[1]!1 ?

i re-inject evaluations of c[0], c[1] , c[2] function f() in order simplify expression (i expect x+1)

note: c[0] not used on purpose...

thanks tushar answering post. right additional variables come existential quantifier. z3 skolemize these variables , stands, model returned z3 includes constants skolemized existential quantifiers. evidently confusing , may in future filter such variables (and functions) away model construction. on other hand, naming conventions used existential variables retain names quantifiers may possible, @ least manually, track origin of variables.