title: Z3 Array in C language not python
body: <p>Kind request dont answer if you doesnt know about Z3 solver.i posted this questions earlier some answers like how to implement array in C poped up.There are some people who developed Z3 solver in this forum.Its Intended to them.If you dont know Z3 solver please avoid to reply for this question.</p>
  
  <p>I have posted this question earlier and got solution as in Python.we had implemented the below problem already in python.we are trying to port Z3 solver to integrate Z3 solver to a in house tool as part of my thesis.Could you help me to show a solution for below requirement in "C" language not in python.</p>
  
  <p>I want to define and create a two dimensional array as following using z3 solver using C API</p>
  
  <p>example : a[3][3] 
  How to define this using Z3 solver C API where in i need to add constraints such as</p>
  
  <p>elements of the two dimensional arrays only 0 or 1.
  sum of each rows is equal to 1
  sum of each columns(controller memory) should me &lt;= 100
  the problem what am trying to solve is, i have two arrays in which one is a[sw]={50,25,100,75} which represents the data produced(50kb) by each functions.b[cont]={100,100,100} controllers with memory(kb) capacity.we are trying to generate a[4][3] matrix with shows the function allocation to the controllers satisfying the above mentioned constraints</p>
  
  <p>sample output(this can be one configuration out of so many) for above problem.but its a valid configuration</p>
  
  <p>a[sw][cont] =</p>
  
  <p>A  B   C<br>
  A 1  0  0 
  B 1  0  0<br>
  C 0  1  0<br>
  D 0  0  1 </p>