Getting all existentially quantified variables (or nullary declare-funs) of a solver in the Java API

[jparsert]

Essentially, I am building an SMT problem by adding things to a solver etc. and in the end I would like to get a list of all variables (i.e. nullary functions). I am using Java and building the problems through the java api. I am wondering if this is somehow possible to do within java.

According to this: this does not seem to be possible:
https://stackoverflow.com/questions/25767200/how-to-get-all-the-variables-that-were-added-to-any-constraint-in-a-solver

[NikolajBjorner]

it is possible to walk all assertions and extract 0-ary uninterpreted functions.
Each expression is either an Application, Bound Variable or Quantifier.
You walk each child of applications to get the 0-ary uninterpreted functions. If the application has 0 arguments and has declaration type (decl-kind) uninterpreted, then it is a hit.
Use a hash-table to avoid re-traversing the same sub-expression.

[jparsert]

I think I got what I wanted with the following code, is that what you meant with using has-tables?:

public static List<String> getAllVarDeclarations(Expr<?> expr) {
        List<String> allDecls = new ArrayList<>();
        List<String> nullaryDecl = new ArrayList<>();
        Set<Expr<?>> done = new HashSet<>();
        Set<Expr<?>> todo = new HashSet<>();
        todo.add(expr);

        while (!todo.isEmpty()) {
            Expr<?> currentExpression = todo.iterator().next();

            // in case we traversed the same (sub)expression before
            if (done.contains(currentExpression)) {
                todo.remove(currentExpression);
                continue;
            }

            todo.remove(currentExpression);
            done.add(currentExpression);

            if (currentExpression.isApp()) {
                todo.addAll(Arrays.asList(currentExpression.getArgs()));

                //System.out.println(currentExpression.);
                System.out.println(currentExpression);
                if (currentExpression.getFuncDecl().getDeclKind() == Z3_OP_UNINTERPRETED) {
                    allDecls.add(currentExpression.toString());
                    if (currentExpression.getArgs().length == 0) {
                      nullaryDecl.add(currentExpression.toString());
                    }
                }

            }

        }

I might clean up the code a bit and create a push request if that is appreciated.