Invalid term with get-value on array constant.

[aniemetz]

The following call to yices_get_value_as_term on an array constant returns an invalid term:

#include <assert.h>
#include <stdlib.h>

#include "yices.h"

int
main()
{
  yices_init();
  type_t s1 = yices_bv_type(18);
  type_t s2 = yices_bool_type();
  type_t s3 = yices_function_type1(s1, s2);
  term_t t5 = yices_new_uninterpreted_term(s3);
  ctx_config_t* cfg = yices_new_config();
  context_t* ctx = yices_new_context(cfg);
  assert(yices_check_context(ctx, NULL) == STATUS_SAT);
  model_t* model = yices_get_model(ctx, 1);
  term_t v = yices_get_value_as_term(model, t5);
  assert(v > 0);
  return 0;
}

Is this expected behavior?

Yices master 09f162107cc9140172e6c890d8ccc633126c3720 on Linux

[ianamason]

I think so. Yes. If you read here it says

Function types are not supported. The function fails and returns NULL_TERM if t has a function type. It also returns NULL_TERM if t’s value can’t be computed.

[disteph]

Indeed, it seems you can't get the function value as a term with yices_get_value_as_term. However, the API gives you access to the value to which a term evaluates in a model, via yices_get_value that stores the value as an yval_t. If you do that for your function / array symbol, you should get an yval_t with tag YVAL_FUNCTION, and then you can use yices_val_expand_function and yices_val_expand_mapping to get the default value and the finite mappings.