(z3py) Generate all solutions for a 2D list using all_smt

Question

To find out all the solutions generated in SMT, I used the all_smt() method suggested in https://stackoverflow.com/a/70656700/12385200

However, this works only for a 1D list. What if we try to list out the solutions for a 2D list?

The general error I got is:

'list' object has no attribute 'as_ast'

I tried to segregate out each 1D list from the 2D list as follows:

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))
    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))
    def all_smt_rec(terms):
        for j in range(len(terms)):
            term = terms[j]
            print("term:", term)
            if sat == s.check():
                m = s.model()
                yield m
                for i in range(len(term)):
                    s.push()
                    block_term(s, m, term[i])
                    for j in range(i):
                        fix_term(s, m, term[j])
                    yield from all_smt_rec(term[i:])
                    s.pop()   
    yield from all_smt_rec(list(initial_terms))

But after a certain number of 'terms', I'm getting the error object of type 'ArithRef' has no len()

How do we make use of all_smt for a 2D ArithRef list? Better so, can we generalise it to an nD list?

Answer 1

initial_terms is supposed to be a simple list of terms that you want to not "duplicate" in the models. If you have a 2d (or n-d for whatever n), simply flatten it before you pass it to all_smt.

An easy way to flatten a 2-D list would be:

>>> import itertools
>>> list(itertools.chain(*[[1,2,3],[4,5,6],[7,8,9]]))
[1, 2, 3, 4, 5, 6, 7, 8, 9]

If you have higher-dimensions, you can write a similar function to flatten them down accordingly.