Z3 Model: reduce internal variables in the model.

It seems as if Z3 produces n^2 additional variables in the model,
if arrays are represented.
Let's reduce this number and only list the relevant variables.

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java

@@ -16,6 +16,7 @@
 import com.microsoft.z3.Z3Exception;
 import com.microsoft.z3.enumerations.Z3_decl_kind;
 import com.microsoft.z3.enumerations.Z3_sort_kind;
+import com.microsoft.z3.enumerations.Z3_symbol_kind;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.HashSet;
@@ -83,8 +84,13 @@ private boolean isInternalSymbol(long funcDecl) {
       case Z3_OP_ARRAY_EXT:
         return true;
       default:
+        long declName = Native.getDeclName(z3context, funcDecl);
+        Z3_symbol_kind kind = Z3_symbol_kind.fromInt(Native.getSymbolKind(z3context, declName));
+        if (kind == Z3_symbol_kind.Z3_INT_SYMBOL) { // bound variables
+          return true;
+        }
         return Z3_IRRELEVANT_MODEL_TERM_PATTERN
-            .matcher(z3creator.symbolToString(Native.getDeclName(z3context, funcDecl)))
+            .matcher(z3creator.symbolToString(declName))
             .matches();
     }
   }

src/org/sosy_lab/java_smt/test/ModelTest.java

@@ -19,6 +19,7 @@
 
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Iterables;
+import com.google.common.collect.Range;
 import java.io.IOException;
 import java.math.BigInteger;
 import java.nio.file.Files;
@@ -1837,10 +1838,16 @@ public void testArrayWithManyValues() throws SolverException, InterruptedExcepti
     }
     BooleanFormula query = amgr.equivalence(array, storedArray);
 
-    testModelIterator(query);
+    List<ValueAssignment> assignments = testModelIterator(query);
+
+    // Check that we only provide relevant assignments and ignore solver-internal variables.
+    // Allow about 100 assignments plus small overhead, for arr[x] := x for 0 to 99.
+    // Some solvers return additional assignments for constant array assignments.
+    assertThat(assignments.size()).isIn(Range.closedOpen(99, 102));
   }
 
-  private void testModelIterator(BooleanFormula f) throws SolverException, InterruptedException {
+  private ImmutableList<ValueAssignment> testModelIterator(BooleanFormula f)
+      throws SolverException, InterruptedException {
     try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
       prover.push(f);
 
@@ -1851,6 +1858,7 @@ private void testModelIterator(BooleanFormula f) throws SolverException, Interru
           // Check that we can iterate through with no crashes.
         }
         assertThat(prover.getModelAssignments()).containsExactlyElementsIn(m).inOrder();
+        return m.asList();
       }
     }
   }