z3 ruby How create array and get only some element-CodePudding

I create array but cant select element. I need array/vector with exactli this same element

[ [0,0,0] , [1,1,1] ...]

   require "z3"
    
   A = Array.new(3){|x| Z3.Int("x#{x}") }
   i = Z3.Int("i")
   j = Z3.Int("j")
    
    
  r = Z3::Solver.new
  r.assert i >= 0 && i <= 2
  r.assert j >= 0 && j <= 2
    r.assert r.Select(A,i) == r.Select(A,j)

  r.check
  p r.model

CodePudding user response：

First, there's a minor syntax issue with &&. Ruby does not allow overloading of &&, so Z3 expressions need to use & and some extra parentheses:

r.assert (i >= 0) & (i <= 2)

A much bigger issue is conceptual. Do you want to use Z3 Arrays, or just plain Ruby array of Z3 Integers.

If you use Z3 arrays, then what you're asking is that some i and j exist, for which a[i] == a[j]:

require "z3"

Z3IntIntArray = Z3::ArraySort.new(Z3::IntSort.new, Z3::IntSort.new)
a = Z3IntIntArray.var("x")
i = Z3.Int("i")
j = Z3.Int("j")

r = Z3::Solver.new
r.assert (i >= 0) & (i <= 2)
r.assert (j >= 0) & (j <= 2)
r.assert a.select(i) == a.select(j)
r.check
p r.model

(upgrade to latest gem for this snippet to work)

But this could be satisfied by a model like a=[42,0,100,550], i=2, j=2.

If I run it, this returns:

Z3::Model<i=0, j=2, x=const(3)>

That is infinitely big array of all 3s, and some arbitrary i and j values. Z3 usually picks the simplest answer if it has multiple possibilities, but it could easily pick something where x[1] is a different number, as you're not really asserting anything about it.

If you use plain Ruby objects, you can specify all equalities:

require "z3"

a = (0..2).map{|i| Z3.Int("a#{i}") }

r = Z3::Solver.new
(0..2).each do |i|
  (0..2).each do |j|
    r.assert a[i] == a[j]
  end
end
r.check
p r.model

You can save yourself O(N^2) code and just check that a[0] == a[1], a[1] == a[2] etc.:

require "z3"

a = (0..2).map{|i| Z3.Int("a#{i}") }

r = Z3::Solver.new
a.each_cons(2) do |ai, aj|
  r.assert ai == aj
end

r.check
p r.model

Either of these returns:

Z3::Model<a0=0, a1=0, a2=0>