Read func interp of a z3 array from the z3 model

by

The representation for array models is indeed a bit confusing. The meaning of

(define-fun some_array_1 () (Array Int Int)   
  (_ as-array k!0))

is that the model for array some_array_1 is the function k!0 which is to be interpreted as an array (signified by the call to as-array. The latter is a parametric function, which has no arguments, therefore, to get at the actual definition of the model function for some_array_1, we have to look up which function as-array calls. In the given example, we can do that as follows, first making sure that we actually have an array model in the expected format by checking a few of assertions:

assert(Z3_get_decl_kind(c, some_array_1_eval_func_decl) == Z3_OP_AS_ARRAY); 
assert(Z3_is_app(c, some_array_1_eval));
assert(Z3_get_decl_num_parameters(c, some_array_1_eval_func_decl) == 1);
assert(Z3_get_decl_parameter_kind(c, some_array_1_eval_func_decl, 0) == 
       Z3_PARAMETER_FUNC_DECL);
func_decl model_fd = func_decl(c, 
                   Z3_get_decl_func_decl_parameter(c, some_array_1_eval_func_decl, 0));

The function declaration model_fd then holds the actual function assigned by the model (k!0) and we can get the function interpretation via

  func_interp fun_interp = m.get_func_interp(model_fd);

More Related Contents:

  1. Is there a way to create a c++ gui game without win32 api, openGL, direct X and stuff? [closed]
  2. Linux API to list running processes?
  3. How to detect the current screen resolution?
  4. Wrapping C++ class API for C consumption
  5. How to detect whether Windows is shutting down or restarting
  6. Drawing in a Win32 Console on C++?
  7. Array of vectors
  8. Possibilities to quit a function
  9. Visual Studio support for new C / C++ standards?
  10. How do I check for C++11 support?
  11. _DEBUG vs NDEBUG
  12. Getting std :: ifstream to handle LF, CR, and CRLF?
  13. Why can’t we declare a std::vector?
  14. How I can print the wchar_t values to console?
  15. Using Unicode in C++ source code
  16. How do you detect/avoid Memory leaks in your (Unmanaged) code? [closed]
  17. static and extern global variables in C and C++
  18. What is the preferred/idiomatic way to insert into a map?
  19. Two ‘main’ functions in C/C++
  20. How can I use covariant return types with smart pointers?
  21. multiset, map and hash map complexity
  22. Empirically determine value category of C++11 expression?
  23. Get current username in C++ on Windows
  24. How to clone as derived object in C++
  25. boost thread throwing exception “thread_resource_error: resource temporarily unavailable”
  26. What is the easiest way to make a C++ program crash?
  27. At what point does dereferencing the null pointer become undefined behavior?
  28. Why doesn’t the C++11 ‘auto’ keyword work for static members?
  29. Double-Checked Lock Singleton in C++11
  30. How is this a most vexing parse?

Leave a Comment