Z3 C-API Get value of a const with no constraints -

i'm on project using c api of z3 , i'm experimenting enumeration sorts in order restrain constant set of finite values.

now problem is, won't value constant long there no constraint defined it. @ point need value returned , i'm wondering how achieve this.

• is there constraint can enforce value assigned constant?

• using online evaluator can force z3 returning value anyway doing following:

  (echo "starting z3...") (declare-datatypes () ((s b c))) (declare-const s) (check-sat) (get-value (a)) 

however can't seem working c-api. i've tried following:

• put ast creating const solver , model. gives me illegal argument error.
• trying model solver without setting assertion gives me invalid usage error

any more ideas? think i'm missing out on something.

the following snippet works me:

using namespace z3; void main() {   context ctx;   func_decl_vector cs(ctx);   func_decl_vector ts(ctx);   char const* abc[3] = {"a","b","c"};   sort s = ctx.enumeration_sort("s", 3, abc, cs, ts);   expr = ctx.constant("a", s);   solver so(ctx);   so.check();   expr b = so.get_model().eval(a, true);   std::cout << b << "\n"; } 

note pass in value "true" second argument of eval. instruments evaluator "complete" model if no value created 'a' when checking satisfiability (of solver state without assertions). model completion default "false".