Z3_INTERRUPT_ERRORS =
+ ImmutableSet.of(
+ "canceled", // Z3::src/util/common_msgs.cpp
+ "push canceled", // src/smt/smt_context.cpp
+ "interrupted from keyboard", // Z3: src/solver/check_sat_result.cpp
+ "Proof error!",
+ "interrupted", // Z3::src/solver/check_sat_result.cpp
+ "maximization suspended" // Z3::src/opt/opt_solver.cpp
+ );
+
+ @Option(secure = true, description = "Whether to use PhantomReferences for discarding Z3 AST")
+ private boolean usePhantomReferences = false;
+
+ /**
+ * We need to track all created symbols for parsing.
+ *
+ * This map stores symbols (names) and their declaration (type information).
+ */
+ private final Map symbolsToDeclarations = new LinkedHashMap<>();
+
+ private final Table allocatedArraySorts = HashBasedTable.create();
+
+ /** Automatic clean-up of Z3 ASTs. */
+ private final ReferenceQueue referenceQueue = new ReferenceQueue<>();
+
+ private final Z3AstReference referenceListHead;
+
+ // todo: getters for statistic.
+ private final Timer cleanupTimer = new Timer();
+ protected final ShutdownNotifier shutdownNotifier;
+
+ @SuppressWarnings("ParameterNumber")
+ Z3LegacyFormulaCreator(
+ long pEnv,
+ long pBoolType,
+ long pIntegerType,
+ long pRealType,
+ long pStringType,
+ long pRegexType,
+ Configuration config,
+ ShutdownNotifier pShutdownNotifier)
+ throws InvalidConfigurationException {
+ super(pEnv, pBoolType, pIntegerType, pRealType, pStringType, pRegexType);
+ shutdownNotifier = pShutdownNotifier;
+ config.inject(this);
+
+ if (usePhantomReferences) {
+ // Setup sentinel nodes for doubly-linked phantom reference list.
+ Z3AstReference head = new Z3AstReference();
+ Z3AstReference tail = new Z3AstReference();
+ head.next = tail;
+ tail.prev = head;
+ referenceListHead = head;
+ } else {
+ referenceListHead = null;
+ }
+ }
+
+ /**
+ * This method throws an {@link InterruptedException} if Z3 was interrupted by a shutdown hook.
+ * Otherwise, the given exception is wrapped and thrown as a SolverException.
+ */
+ @CanIgnoreReturnValue
+ final SolverException handleZ3Exception(Z3Exception e)
+ throws SolverException, InterruptedException {
+ if (Z3_INTERRUPT_ERRORS.contains(e.getMessage())) {
+ shutdownNotifier.shutdownIfNecessary();
+ }
+ throw new SolverException("Z3 has thrown an exception", e);
+ }
+
+ /**
+ * This method handles a Z3Exception, however it only throws a RuntimeException. This method is
+ * used in places where we cannot throw a checked exception in JavaSMT due to API restrictions.
+ *
+ * @param e the Z3Exception to handle
+ * @return nothing, always throw a RuntimeException
+ * @throws RuntimeException always thrown for the given Z3Exception
+ */
+ final RuntimeException handleZ3ExceptionAsRuntimeException(Z3Exception e) {
+ try {
+ throw handleZ3Exception(e);
+ } catch (InterruptedException ex) {
+ Thread.currentThread().interrupt();
+ throw sneakyThrow(e);
+ } catch (SolverException ex) {
+ throw sneakyThrow(e);
+ }
+ }
+
+ @SuppressWarnings("unchecked")
+ private static RuntimeException sneakyThrow(Throwable e) throws E {
+ throw (E) e;
+ }
+
+ @Override
+ public Long makeVariable(Long type, String varName) {
+ long z3context = getEnv();
+ long symbol = Native.mkStringSymbol(z3context, varName);
+ long var = Native.mkConst(z3context, symbol, type);
+ Native.incRef(z3context, var);
+ symbolsToDeclarations.put(varName, Native.getAppDecl(z3context, var));
+ return var;
+ }
+
+ @Override
+ public Long extractInfo(Formula pT) {
+ if (pT instanceof Z3LegacyFormula) {
+ return ((Z3LegacyFormula) pT).getFormulaInfo();
+ }
+ throw new IllegalArgumentException(
+ "Cannot get the formula info of type " + pT.getClass().getSimpleName() + " in the Solver!");
+ }
+
+ @SuppressWarnings("unchecked")
+ @Override
+ public FormulaType getFormulaType(T pFormula) {
+ Long term = extractInfo(pFormula);
+ return (FormulaType) getFormulaType(term);
+ }
+
+ public FormulaType getFormulaTypeFromSort(Long pSort) {
+ long z3context = getEnv();
+ Z3_sort_kind sortKind = Z3_sort_kind.fromInt(Native.getSortKind(z3context, pSort));
+ switch (sortKind) {
+ case Z3_BOOL_SORT:
+ return FormulaType.BooleanType;
+ case Z3_INT_SORT:
+ return FormulaType.IntegerType;
+ case Z3_REAL_SORT:
+ return FormulaType.RationalType;
+ case Z3_BV_SORT:
+ return FormulaType.getBitvectorTypeWithSize(Native.getBvSortSize(z3context, pSort));
+ case Z3_ARRAY_SORT:
+ long domainSort = Native.getArraySortDomain(z3context, pSort);
+ long rangeSort = Native.getArraySortRange(z3context, pSort);
+ return FormulaType.getArrayType(
+ getFormulaTypeFromSort(domainSort), getFormulaTypeFromSort(rangeSort));
+ case Z3_FLOATING_POINT_SORT:
+ return FormulaType.getFloatingPointType(
+ Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort) - 1);
+ case Z3_ROUNDING_MODE_SORT:
+ return FormulaType.FloatingPointRoundingModeType;
+ case Z3_RE_SORT:
+ return FormulaType.RegexType;
+ case Z3_DATATYPE_SORT:
+ int n = Native.getDatatypeSortNumConstructors(z3context, pSort);
+ ImmutableSet.Builder elements = ImmutableSet.builder();
+ for (int i = 0; i < n; i++) {
+ long decl = Native.getDatatypeSortConstructor(z3context, pSort, i);
+ elements.add(symbolToString(Native.getDeclName(z3context, decl)));
+ }
+ return FormulaType.getEnumerationType(
+ Native.sortToString(z3context, pSort), elements.build());
+ case Z3_RELATION_SORT:
+ case Z3_FINITE_DOMAIN_SORT:
+ case Z3_SEQ_SORT:
+ case Z3_UNKNOWN_SORT:
+ case Z3_UNINTERPRETED_SORT:
+ if (Native.isStringSort(z3context, pSort)) {
+ return FormulaType.StringType;
+ } else {
+ // TODO: support for remaining sorts.
+ throw new IllegalArgumentException(
+ "Unknown formula type "
+ + Native.sortToString(z3context, pSort)
+ + " with sort "
+ + sortKind);
+ }
+ default:
+ throw new UnsupportedOperationException("Unexpected state.");
+ }
+ }
+
+ @Override
+ public FormulaType getFormulaType(Long pFormula) {
+ long sort = Native.getSort(getEnv(), pFormula);
+ return getFormulaTypeFromSort(sort);
+ }
+
+ @Override
+ @SuppressWarnings("MethodTypeParameterName")
+ protected | FormulaType | getArrayFormulaElementType(
+ ArrayFormula pArray) {
+ return ((Z3ArrayLegacyFormula) pArray).getElementType();
+ }
+
+ @Override
+ @SuppressWarnings("MethodTypeParameterName")
+ protected | FormulaType | getArrayFormulaIndexType(
+ ArrayFormula pArray) {
+ return ((Z3ArrayLegacyFormula) pArray).getIndexType();
+ }
+
+ @Override
+ @SuppressWarnings("MethodTypeParameterName")
+ protected ArrayFormula encapsulateArray(
+ Long pTerm, FormulaType| pIndexType, FormulaType | pElementType) {
+ assert getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElementType));
+ cleanupReferences();
+ return storePhantomReference(
+ new Z3ArrayLegacyFormula<>(getEnv(), pTerm, pIndexType, pElementType), pTerm);
+ }
+
+ @SuppressWarnings("unchecked")
+ @Override
+ public T encapsulate(FormulaType pType, Long pTerm) {
+ assert pType.equals(getFormulaType(pTerm))
+ || (pType.equals(FormulaType.RationalType)
+ && getFormulaType(pTerm).equals(FormulaType.IntegerType))
+ : String.format(
+ "Trying to encapsulate formula of type %s as %s", getFormulaType(pTerm), pType);
+ cleanupReferences();
+ if (pType.isBooleanType()) {
+ return (T) storePhantomReference(new Z3BooleanLegacyFormula(getEnv(), pTerm), pTerm);
+ } else if (pType.isIntegerType()) {
+ return (T) storePhantomReference(new Z3IntegerLegacyFormula(getEnv(), pTerm), pTerm);
+ } else if (pType.isRationalType()) {
+ return (T) storePhantomReference(new Z3RationalLegacyFormula(getEnv(), pTerm), pTerm);
+ } else if (pType.isStringType()) {
+ return (T) storePhantomReference(new Z3StringLegacyFormula(getEnv(), pTerm), pTerm);
+ } else if (pType.isRegexType()) {
+ return (T) storePhantomReference(new Z3RegexLegacyFormula(getEnv(), pTerm), pTerm);
+ } else if (pType.isBitvectorType()) {
+ return (T) storePhantomReference(new Z3BitvectorLegacyFormula(getEnv(), pTerm), pTerm);
+ } else if (pType.isFloatingPointType()) {
+ return (T) storePhantomReference(new Z3FloatingPointLegacyFormula(getEnv(), pTerm), pTerm);
+ } else if (pType.isFloatingPointRoundingModeType()) {
+ return (T)
+ storePhantomReference(
+ new Z3FloatingPointRoundingModeLegacyFormula(getEnv(), pTerm), pTerm);
+ } else if (pType.isArrayType()) {
+ ArrayFormulaType arrFt = (ArrayFormulaType) pType;
+ return (T)
+ storePhantomReference(
+ new Z3ArrayLegacyFormula<>(
+ getEnv(), pTerm, arrFt.getIndexType(), arrFt.getElementType()),
+ pTerm);
+ } else if (pType.isEnumerationType()) {
+ return (T) storePhantomReference(new Z3EnumerationLegacyFormula(getEnv(), pTerm), pTerm);
+ }
+
+ throw new IllegalArgumentException("Cannot create formulas of type " + pType + " in Z3");
+ }
+
+ @Override
+ public BooleanFormula encapsulateBoolean(Long pTerm) {
+ assert getFormulaType(pTerm).isBooleanType();
+ cleanupReferences();
+ return storePhantomReference(new Z3BooleanLegacyFormula(getEnv(), pTerm), pTerm);
+ }
+
+ @Override
+ public BitvectorFormula encapsulateBitvector(Long pTerm) {
+ assert getFormulaType(pTerm).isBitvectorType();
+ cleanupReferences();
+ return storePhantomReference(new Z3BitvectorLegacyFormula(getEnv(), pTerm), pTerm);
+ }
+
+ @Override
+ protected FloatingPointFormula encapsulateFloatingPoint(Long pTerm) {
+ assert getFormulaType(pTerm).isFloatingPointType();
+ cleanupReferences();
+ return storePhantomReference(new Z3FloatingPointLegacyFormula(getEnv(), pTerm), pTerm);
+ }
+
+ @Override
+ protected StringFormula encapsulateString(Long pTerm) {
+ assert getFormulaType(pTerm).isStringType()
+ : String.format(
+ "Term %s has unexpected type %s.",
+ Native.astToString(getEnv(), pTerm),
+ Native.sortToString(getEnv(), Native.getSort(getEnv(), pTerm)));
+ cleanupReferences();
+ return storePhantomReference(new Z3StringLegacyFormula(getEnv(), pTerm), pTerm);
+ }
+
+ @Override
+ protected RegexFormula encapsulateRegex(Long pTerm) {
+ assert getFormulaType(pTerm).isRegexType()
+ : String.format(
+ "Term %s has unexpected type %s.",
+ Native.astToString(getEnv(), pTerm),
+ Native.sortToString(getEnv(), Native.getSort(getEnv(), pTerm)));
+ cleanupReferences();
+ return storePhantomReference(new Z3RegexLegacyFormula(getEnv(), pTerm), pTerm);
+ }
+
+ @Override
+ protected EnumerationFormula encapsulateEnumeration(Long pTerm) {
+ assert getFormulaType(pTerm).isEnumerationType()
+ : String.format(
+ "Term %s has unexpected type %s.",
+ Native.astToString(getEnv(), pTerm),
+ Native.sortToString(getEnv(), Native.getSort(getEnv(), pTerm)));
+ cleanupReferences();
+ return storePhantomReference(new Z3EnumerationLegacyFormula(getEnv(), pTerm), pTerm);
+ }
+
+ @Override
+ public Long getArrayType(Long pIndexType, Long pElementType) {
+ Long allocatedArraySort = allocatedArraySorts.get(pIndexType, pElementType);
+ if (allocatedArraySort == null) {
+ allocatedArraySort = Native.mkArraySort(getEnv(), pIndexType, pElementType);
+ Native.incRef(getEnv(), allocatedArraySort);
+ allocatedArraySorts.put(pIndexType, pElementType, allocatedArraySort);
+ }
+ return allocatedArraySort;
+ }
+
+ @Override
+ public Long getBitvectorType(int pBitwidth) {
+ checkArgument(pBitwidth > 0, "Cannot use bitvector type with size %s", pBitwidth);
+ long bvSort = Native.mkBvSort(getEnv(), pBitwidth);
+ Native.incRef(getEnv(), Native.sortToAst(getEnv(), bvSort));
+ return bvSort;
+ }
+
+ @Override
+ public Long getFloatingPointType(FloatingPointType type) {
+ long fpSort = Native.mkFpaSort(getEnv(), type.getExponentSize(), type.getMantissaSize() + 1);
+ Native.incRef(getEnv(), Native.sortToAst(getEnv(), fpSort));
+ return fpSort;
+ }
+
+ private static final class Z3AstReference extends PhantomReference {
+ private final long z3Ast;
+ private @Nullable Z3AstReference prev;
+ private @Nullable Z3AstReference next;
+
+ // To generate dummy head and tail nodes
+ private Z3AstReference() {
+ this(null, null, 0);
+ }
+
+ private Z3AstReference(
+ Z3LegacyFormula referent, ReferenceQueue q, long z3Ast) {
+ super(referent, q);
+ this.z3Ast = z3Ast;
+ }
+
+ private void insert(Z3AstReference ref) {
+ assert next != null;
+ ref.prev = this;
+ ref.next = this.next;
+ ref.next.prev = ref;
+ this.next = ref;
+ }
+
+ private void cleanup(long environment) {
+ Native.decRef(environment, z3Ast);
+ assert (prev != null && next != null);
+ prev.next = next;
+ next.prev = prev;
+ }
+ }
+
+ private T storePhantomReference(T out, long pTerm) {
+ if (usePhantomReferences) {
+ referenceListHead.insert(new Z3AstReference(out, referenceQueue, pTerm));
+ }
+ return out;
+ }
+
+ private void cleanupReferences() {
+ if (!usePhantomReferences) {
+ return;
+ }
+ cleanupTimer.start();
+ try {
+ Z3AstReference ref;
+ while ((ref = (Z3AstReference) referenceQueue.poll()) != null) {
+ ref.cleanup(environment);
+ }
+ } finally {
+ cleanupTimer.stop();
+ }
+ }
+
+ private String getAppName(long f) {
+ long funcDecl = Native.getAppDecl(environment, f);
+ long symbol = Native.getDeclName(environment, funcDecl);
+ return symbolToString(symbol);
+ }
+
+ @SuppressWarnings("deprecation")
+ @Override
+ public R visit(FormulaVisitor visitor, final Formula formula, final Long f) {
+ switch (Z3_ast_kind.fromInt(Native.getAstKind(environment, f))) {
+ case Z3_NUMERAL_AST:
+ return visitor.visitConstant(formula, convertValue(f));
+ case Z3_APP_AST:
+ int arity = Native.getAppNumArgs(environment, f);
+ int declKind = Native.getDeclKind(environment, Native.getAppDecl(environment, f));
+
+ if (arity == 0) {
+ // constants
+ Object value = Z3_CONSTANTS.get(declKind);
+ if (value != null) {
+ return visitor.visitConstant(formula, value);
+
+ } else if (Z3_FP_CONSTANTS.contains(declKind)) {
+ return visitor.visitConstant(formula, convertValue(f));
+
+ // Rounding mode
+ } else if (declKind == Z3_decl_kind.Z3_OP_FPA_NUM.toInt()
+ || Native.getSortKind(environment, Native.getSort(environment, f))
+ == Z3_sort_kind.Z3_ROUNDING_MODE_SORT.toInt()) {
+ return visitor.visitConstant(formula, convertValue(f));
+
+ // string constant
+ } else if (declKind == Z3_decl_kind.Z3_OP_INTERNAL.toInt()
+ && Native.getSortKind(environment, Native.getSort(environment, f))
+ == Z3_sort_kind.Z3_SEQ_SORT.toInt()) {
+ return visitor.visitConstant(formula, convertValue(f));
+
+ // Free variable
+ } else if (declKind == Z3_decl_kind.Z3_OP_UNINTERPRETED.toInt()
+ || declKind == Z3_decl_kind.Z3_OP_INTERNAL.toInt()) {
+ return visitor.visitFreeVariable(formula, getAppName(f));
+
+ // enumeration constant
+ } else if (declKind == Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR.toInt()) {
+ return visitor.visitConstant(formula, convertValue(f));
+ } // else: fall-through with a function application
+
+ } else if (arity == 3) {
+
+ // FP from BV
+ if (declKind == Z3_decl_kind.Z3_OP_FPA_FP.toInt()) {
+ final var signBv = Native.getAppArg(environment, f, 0);
+ final var expoBv = Native.getAppArg(environment, f, 1);
+ final var mantBv = Native.getAppArg(environment, f, 2);
+ if (isConstant(signBv) && isConstant(expoBv) && isConstant(mantBv)) {
+ return visitor.visitConstant(formula, convertValue(f));
+ }
+ }
+ }
+
+ // Function application with zero or more parameters
+ ImmutableList.Builder args = ImmutableList.builder();
+ ImmutableList.Builder> argTypes = ImmutableList.builder();
+ for (int i = 0; i < arity; i++) {
+ long arg = Native.getAppArg(environment, f, i);
+ FormulaType argumentType = getFormulaType(arg);
+ args.add(encapsulate(argumentType, arg));
+ argTypes.add(argumentType);
+ }
+ return visitor.visitFunction(
+ formula,
+ args.build(),
+ FunctionDeclarationImpl.of(
+ getAppName(f),
+ getDeclarationKind(f),
+ argTypes.build(),
+ getFormulaType(f),
+ Native.getAppDecl(environment, f)));
+ case Z3_VAR_AST:
+ int deBruijnIdx = Native.getIndexValue(environment, f);
+ return visitor.visitBoundVariable(formula, deBruijnIdx);
+ case Z3_QUANTIFIER_AST:
+ BooleanFormula body = encapsulateBoolean(Native.getQuantifierBody(environment, f));
+ Quantifier q =
+ Native.isQuantifierForall(environment, f) ? Quantifier.FORALL : Quantifier.EXISTS;
+ return visitor.visitQuantifier((BooleanFormula) formula, q, getBoundVars(f), body);
+
+ case Z3_SORT_AST:
+ case Z3_FUNC_DECL_AST:
+ case Z3_UNKNOWN_AST:
+ default:
+ throw new UnsupportedOperationException(
+ "Input should be a formula AST, " + "got unexpected type instead");
+ }
+ }
+
+ protected String symbolToString(long symbol) {
+ switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(environment, symbol))) {
+ case Z3_STRING_SYMBOL:
+ return Native.getSymbolString(environment, symbol);
+ case Z3_INT_SYMBOL:
+
+ // Bound variable.
+ return "#" + Native.getSymbolInt(environment, symbol);
+ default:
+ throw new UnsupportedOperationException("Unexpected state");
+ }
+ }
+
+ private List getBoundVars(long f) {
+ int numBound = Native.getQuantifierNumBound(environment, f);
+ List boundVars = new ArrayList<>(numBound);
+ for (int i = 0; i < numBound; i++) {
+ long varName = Native.getQuantifierBoundName(environment, f, i);
+ long varSort = Native.getQuantifierBoundSort(environment, f, i);
+ boundVars.add(
+ encapsulate(
+ getFormulaTypeFromSort(varSort), Native.mkConst(environment, varName, varSort)));
+ }
+ return boundVars;
+ }
+
+ private FunctionDeclarationKind getDeclarationKind(long f) {
+ final int arity = Native.getArity(environment, Native.getAppDecl(environment, f));
+ assert arity > 0
+ : String.format(
+ "Unexpected arity '%s' for formula '%s' for handling a function application.",
+ arity, Native.astToString(environment, f));
+ if (getAppName(f).equals("div0")) {
+ // Z3 segfaults in getDeclKind for this term (cf. https://github.com/Z3Prover/z3/issues/669)
+ return FunctionDeclarationKind.OTHER;
+ }
+ Z3_decl_kind decl =
+ Z3_decl_kind.fromInt(Native.getDeclKind(environment, Native.getAppDecl(environment, f)));
+ switch (decl) {
+ case Z3_OP_AND:
+ return FunctionDeclarationKind.AND;
+ case Z3_OP_NOT:
+ return FunctionDeclarationKind.NOT;
+ case Z3_OP_OR:
+ return FunctionDeclarationKind.OR;
+ case Z3_OP_IFF:
+ return FunctionDeclarationKind.IFF;
+ case Z3_OP_ITE:
+ return FunctionDeclarationKind.ITE;
+ case Z3_OP_XOR:
+ return FunctionDeclarationKind.XOR;
+ case Z3_OP_DISTINCT:
+ return FunctionDeclarationKind.DISTINCT;
+ case Z3_OP_IMPLIES:
+ return FunctionDeclarationKind.IMPLIES;
+
+ case Z3_OP_SUB:
+ return FunctionDeclarationKind.SUB;
+ case Z3_OP_ADD:
+ return FunctionDeclarationKind.ADD;
+ case Z3_OP_DIV:
+ return FunctionDeclarationKind.DIV;
+ case Z3_OP_MUL:
+ return FunctionDeclarationKind.MUL;
+ case Z3_OP_MOD:
+ return FunctionDeclarationKind.MODULO;
+ case Z3_OP_TO_INT:
+ return FunctionDeclarationKind.FLOOR;
+ case Z3_OP_TO_REAL:
+ return FunctionDeclarationKind.TO_REAL;
+
+ case Z3_OP_UNINTERPRETED:
+ return FunctionDeclarationKind.UF;
+
+ case Z3_OP_LT:
+ return FunctionDeclarationKind.LT;
+ case Z3_OP_LE:
+ return FunctionDeclarationKind.LTE;
+ case Z3_OP_GT:
+ return FunctionDeclarationKind.GT;
+ case Z3_OP_GE:
+ return FunctionDeclarationKind.GTE;
+ case Z3_OP_EQ:
+ return FunctionDeclarationKind.EQ;
+
+ case Z3_OP_STORE:
+ return FunctionDeclarationKind.STORE;
+ case Z3_OP_SELECT:
+ return FunctionDeclarationKind.SELECT;
+ case Z3_OP_CONST_ARRAY:
+ return FunctionDeclarationKind.CONST;
+
+ case Z3_OP_TRUE:
+ case Z3_OP_FALSE:
+ case Z3_OP_ANUM:
+ case Z3_OP_AGNUM:
+ throw new UnsupportedOperationException("Unexpected state: constants not expected");
+ case Z3_OP_OEQ:
+ throw new UnsupportedOperationException("Unexpected state: not a proof");
+ case Z3_OP_UMINUS:
+ return FunctionDeclarationKind.UMINUS;
+ case Z3_OP_IDIV:
+
+ // TODO: different handling for integer division?
+ return FunctionDeclarationKind.DIV;
+
+ case Z3_OP_EXTRACT:
+ return FunctionDeclarationKind.BV_EXTRACT;
+ case Z3_OP_CONCAT:
+ return FunctionDeclarationKind.BV_CONCAT;
+ case Z3_OP_BNOT:
+ return FunctionDeclarationKind.BV_NOT;
+ case Z3_OP_BNEG:
+ return FunctionDeclarationKind.BV_NEG;
+ case Z3_OP_BAND:
+ return FunctionDeclarationKind.BV_AND;
+ case Z3_OP_BOR:
+ return FunctionDeclarationKind.BV_OR;
+ case Z3_OP_BXOR:
+ return FunctionDeclarationKind.BV_XOR;
+ case Z3_OP_ULT:
+ return FunctionDeclarationKind.BV_ULT;
+ case Z3_OP_SLT:
+ return FunctionDeclarationKind.BV_SLT;
+ case Z3_OP_ULEQ:
+ return FunctionDeclarationKind.BV_ULE;
+ case Z3_OP_SLEQ:
+ return FunctionDeclarationKind.BV_SLE;
+ case Z3_OP_UGT:
+ return FunctionDeclarationKind.BV_UGT;
+ case Z3_OP_SGT:
+ return FunctionDeclarationKind.BV_SGT;
+ case Z3_OP_UGEQ:
+ return FunctionDeclarationKind.BV_UGE;
+ case Z3_OP_SGEQ:
+ return FunctionDeclarationKind.BV_SGE;
+ case Z3_OP_BADD:
+ return FunctionDeclarationKind.BV_ADD;
+ case Z3_OP_BSUB:
+ return FunctionDeclarationKind.BV_SUB;
+ case Z3_OP_BMUL:
+ return FunctionDeclarationKind.BV_MUL;
+ case Z3_OP_BUDIV:
+ case Z3_OP_BUDIV_I: // same as above, and divisor is non-zero
+ return FunctionDeclarationKind.BV_UDIV;
+ case Z3_OP_BSDIV:
+ case Z3_OP_BSDIV_I: // same as above, and divisor is non-zero
+ return FunctionDeclarationKind.BV_SDIV;
+ case Z3_OP_BUREM:
+ case Z3_OP_BUREM_I: // same as above, and divisor is non-zero
+ return FunctionDeclarationKind.BV_UREM;
+ case Z3_OP_BSREM:
+ case Z3_OP_BSREM_I: // same as above, and divisor is non-zero
+ return FunctionDeclarationKind.BV_SREM;
+ case Z3_OP_BSMOD:
+ case Z3_OP_BSMOD_I: // same as above, and divisor is non-zero
+ return FunctionDeclarationKind.BV_SMOD;
+ case Z3_OP_BSHL:
+ return FunctionDeclarationKind.BV_SHL;
+ case Z3_OP_BLSHR:
+ return FunctionDeclarationKind.BV_LSHR;
+ case Z3_OP_BASHR:
+ return FunctionDeclarationKind.BV_ASHR;
+ case Z3_OP_SIGN_EXT:
+ return FunctionDeclarationKind.BV_SIGN_EXTENSION;
+ case Z3_OP_ZERO_EXT:
+ return FunctionDeclarationKind.BV_ZERO_EXTENSION;
+ case Z3_OP_ROTATE_LEFT:
+ return FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT;
+ case Z3_OP_ROTATE_RIGHT:
+ return FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT;
+ case Z3_OP_EXT_ROTATE_LEFT:
+ return FunctionDeclarationKind.BV_ROTATE_LEFT;
+ case Z3_OP_EXT_ROTATE_RIGHT:
+ return FunctionDeclarationKind.BV_ROTATE_RIGHT;
+
+ case Z3_OP_FPA_NEG:
+ return FunctionDeclarationKind.FP_NEG;
+ case Z3_OP_FPA_ABS:
+ return FunctionDeclarationKind.FP_ABS;
+ case Z3_OP_FPA_MAX:
+ return FunctionDeclarationKind.FP_MAX;
+ case Z3_OP_FPA_MIN:
+ return FunctionDeclarationKind.FP_MIN;
+ case Z3_OP_FPA_SQRT:
+ return FunctionDeclarationKind.FP_SQRT;
+ case Z3_OP_FPA_SUB:
+ return FunctionDeclarationKind.FP_SUB;
+ case Z3_OP_FPA_ADD:
+ return FunctionDeclarationKind.FP_ADD;
+ case Z3_OP_FPA_DIV:
+ return FunctionDeclarationKind.FP_DIV;
+ case Z3_OP_FPA_MUL:
+ return FunctionDeclarationKind.FP_MUL;
+ case Z3_OP_FPA_REM:
+ return FunctionDeclarationKind.FP_REM;
+ case Z3_OP_FPA_LT:
+ return FunctionDeclarationKind.FP_LT;
+ case Z3_OP_FPA_LE:
+ return FunctionDeclarationKind.FP_LE;
+ case Z3_OP_FPA_GE:
+ return FunctionDeclarationKind.FP_GE;
+ case Z3_OP_FPA_GT:
+ return FunctionDeclarationKind.FP_GT;
+ case Z3_OP_FPA_EQ:
+ return FunctionDeclarationKind.FP_EQ;
+ case Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
+ return FunctionDeclarationKind.FP_ROUND_EVEN;
+ case Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
+ return FunctionDeclarationKind.FP_ROUND_AWAY;
+ case Z3_OP_FPA_RM_TOWARD_POSITIVE:
+ return FunctionDeclarationKind.FP_ROUND_POSITIVE;
+ case Z3_OP_FPA_RM_TOWARD_NEGATIVE:
+ return FunctionDeclarationKind.FP_ROUND_NEGATIVE;
+ case Z3_OP_FPA_RM_TOWARD_ZERO:
+ return FunctionDeclarationKind.FP_ROUND_ZERO;
+ case Z3_OP_FPA_ROUND_TO_INTEGRAL:
+ return FunctionDeclarationKind.FP_ROUND_TO_INTEGRAL;
+ case Z3_OP_FPA_TO_FP_UNSIGNED:
+ return FunctionDeclarationKind.BV_UCASTTO_FP;
+ case Z3_OP_FPA_TO_SBV:
+ return FunctionDeclarationKind.FP_CASTTO_SBV;
+ case Z3_OP_FPA_TO_UBV:
+ return FunctionDeclarationKind.FP_CASTTO_UBV;
+ case Z3_OP_FPA_TO_IEEE_BV:
+ return FunctionDeclarationKind.FP_AS_IEEEBV;
+ case Z3_OP_FPA_TO_FP:
+ // use the last argument. other arguments can be part of rounding or casting.
+ long arg = Native.getAppArg(environment, f, Native.getAppNumArgs(environment, f) - 1);
+ Z3_sort_kind sortKind =
+ Z3_sort_kind.fromInt(Native.getSortKind(environment, Native.getSort(environment, arg)));
+ if (Z3_sort_kind.Z3_BV_SORT == sortKind) {
+ return FunctionDeclarationKind.BV_SCASTTO_FP;
+ } else {
+ return FunctionDeclarationKind.FP_CASTTO_FP;
+ }
+ case Z3_OP_FPA_IS_NAN:
+ return FunctionDeclarationKind.FP_IS_NAN;
+ case Z3_OP_FPA_IS_INF:
+ return FunctionDeclarationKind.FP_IS_INF;
+ case Z3_OP_FPA_IS_ZERO:
+ return FunctionDeclarationKind.FP_IS_ZERO;
+ case Z3_OP_FPA_IS_NEGATIVE:
+ return FunctionDeclarationKind.FP_IS_NEGATIVE;
+ case Z3_OP_FPA_IS_SUBNORMAL:
+ return FunctionDeclarationKind.FP_IS_SUBNORMAL;
+ case Z3_OP_FPA_IS_NORMAL:
+ return FunctionDeclarationKind.FP_IS_NORMAL;
+
+ case Z3_OP_SEQ_CONCAT:
+ return FunctionDeclarationKind.STR_CONCAT;
+ case Z3_OP_SEQ_PREFIX:
+ return FunctionDeclarationKind.STR_PREFIX;
+ case Z3_OP_SEQ_SUFFIX:
+ return FunctionDeclarationKind.STR_SUFFIX;
+ case Z3_OP_SEQ_CONTAINS:
+ return FunctionDeclarationKind.STR_CONTAINS;
+ case Z3_OP_SEQ_EXTRACT:
+ return FunctionDeclarationKind.STR_SUBSTRING;
+ case Z3_OP_SEQ_REPLACE:
+ return FunctionDeclarationKind.STR_REPLACE;
+ case Z3_OP_SEQ_AT:
+ return FunctionDeclarationKind.STR_CHAR_AT;
+ case Z3_OP_SEQ_LENGTH:
+ return FunctionDeclarationKind.STR_LENGTH;
+ case Z3_OP_SEQ_INDEX:
+ return FunctionDeclarationKind.STR_INDEX_OF;
+ case Z3_OP_SEQ_TO_RE:
+ return FunctionDeclarationKind.STR_TO_RE;
+ case Z3_OP_SEQ_IN_RE:
+ return FunctionDeclarationKind.STR_IN_RE;
+ case Z3_OP_RE_PLUS:
+ return FunctionDeclarationKind.RE_PLUS;
+ case Z3_OP_RE_STAR:
+ return FunctionDeclarationKind.RE_STAR;
+ case Z3_OP_RE_OPTION:
+ return FunctionDeclarationKind.RE_OPTIONAL;
+ case Z3_OP_RE_CONCAT:
+ return FunctionDeclarationKind.RE_CONCAT;
+ case Z3_OP_RE_UNION:
+ return FunctionDeclarationKind.RE_UNION;
+
+ default:
+ return FunctionDeclarationKind.OTHER;
+ }
+ }
+
+ /**
+ * @param value Z3_ast
+ * @return Whether the value is a constant and can be passed to {@link #convertValue(Long)}.
+ */
+ public boolean isConstant(long value) {
+ return Native.isNumeralAst(environment, value)
+ || Native.isAlgebraicNumber(environment, value)
+ || Native.isString(environment, value)
+ || isOP(environment, value, Z3_decl_kind.Z3_OP_FPA_FP) // FP from IEEE-BV
+ || isOP(environment, value, Z3_decl_kind.Z3_OP_TRUE)
+ || isOP(environment, value, Z3_decl_kind.Z3_OP_FALSE)
+ || isOP(environment, value, Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR); // enumeration value
+ }
+
+ /**
+ * @param value Z3_ast representing a constant value.
+ * @return {@link BigInteger} or {@link Double} or {@link Rational} or {@link Boolean} or {@link
+ * FloatingPointRoundingMode} or {@link String}.
+ */
+ @Override
+ public Object convertValue(Long value) {
+ if (!isConstant(value)) {
+ return null;
+ }
+
+ Native.incRef(environment, value);
+
+ Object constantValue =
+ Z3_CONSTANTS.get(Native.getDeclKind(environment, Native.getAppDecl(environment, value)));
+ if (constantValue != null) {
+ return constantValue;
+ }
+
+ try {
+ FormulaType type = getFormulaType(value);
+ if (type.isBooleanType()) {
+ return isOP(environment, value, Z3_decl_kind.Z3_OP_TRUE);
+ } else if (type.isIntegerType()) {
+ return new BigInteger(Native.getNumeralString(environment, value));
+ } else if (type.isRationalType()) {
+ Rational ratValue = Rational.ofString(Native.getNumeralString(environment, value));
+ return ratValue.isIntegral() ? ratValue.getNum() : ratValue;
+ } else if (type.isStringType()) {
+ return unescapeUnicodeForSmtlib(Native.getString(environment, value));
+ } else if (type.isBitvectorType()) {
+ return new BigInteger(Native.getNumeralString(environment, value));
+ } else if (type.isFloatingPointType()) {
+ return convertFloatingPoint((FloatingPointType) type, value);
+ } else if (type.isEnumerationType()) {
+ return Native.astToString(environment, value);
+ } else {
+
+ // Explicitly crash on unknown type.
+ throw new IllegalArgumentException("Unexpected type encountered: " + type);
+ }
+
+ } finally {
+ Native.decRef(environment, value);
+ }
+ }
+
+ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long pValue) {
+ if (isOP(environment, pValue, Z3_decl_kind.Z3_OP_FPA_FP)) {
+ final var signBv = Native.getAppArg(environment, pValue, 0);
+ final var expoBv = Native.getAppArg(environment, pValue, 1);
+ final var mantBv = Native.getAppArg(environment, pValue, 2);
+ assert isConstant(signBv) && isConstant(expoBv) && isConstant(mantBv);
+ final var sign = Native.getNumeralString(environment, signBv);
+ assert "0".equals(sign) || "1".equals(sign);
+ final var expo = new BigInteger(Native.getNumeralString(environment, expoBv));
+ final var mant = new BigInteger(Native.getNumeralString(environment, mantBv));
+ return FloatingPointNumber.of(
+ Sign.of(sign.charAt(0) == '1'),
+ expo,
+ mant,
+ pType.getExponentSize(),
+ pType.getMantissaSize());
+
+ // } else if (Native.fpaIsNumeralInf(environment, pValue)) {
+ // // Floating Point Inf uses:
+ // // - an sign for posiive/negative infinity,
+ // // - "11..11" as exponent,
+ // // - "00..00" as mantissa.
+ // String sign = getSign(pValue).isNegative() ? "1" : "0";
+ // return FloatingPointNumber.of(
+ // sign + "1".repeat(pType.getExponentSize()) + "0".repeat(pType.getMantissaSize()),
+ // pType.getExponentSize(),
+ // pType.getMantissaSize());
+ //
+ // } else if (Native.fpaIsNumeralNan(environment, pValue)) {
+ // // TODO We are underspecified here and choose several bits on our own.
+ // // This is not sound, if we combine FP anf BV theory.
+ // // Floating Point NaN uses:
+ // // - an unspecified sign (we choose "0"),
+ // // - "11..11" as exponent,
+ // // - an unspecified mantissa (we choose all "1").
+ // return FloatingPointNumber.of(
+ // "0" + "1".repeat(pType.getExponentSize()) + "1".repeat(pType.getMantissaSize()),
+ // pType.getExponentSize(),
+ // pType.getMantissaSize());
+
+ } else {
+ Sign sign = getSign(pValue);
+ var exponent = Native.fpaGetNumeralExponentString(environment, pValue);
+ var mantissa = Native.fpaGetNumeralSignificandString(environment, pValue);
+ return FloatingPointNumber.of(
+ sign,
+ new BigInteger(exponent),
+ new BigInteger(mantissa),
+ pType.getExponentSize(),
+ pType.getMantissaSize());
+ }
+ }
+
+ private Sign getSign(Long pValue) {
+ Native.IntPtr signPtr = new Native.IntPtr();
+ Preconditions.checkState(
+ Native.fpaGetNumeralSign(environment, pValue, signPtr), "Sign is not a Boolean value");
+ var sign = signPtr.value != 0;
+ return Sign.of(sign);
+ }
+
+ @Override
+ public Long declareUFImpl(String pName, Long returnType, List pArgTypes) {
+ long symbol = Native.mkStringSymbol(environment, pName);
+ long[] sorts = Longs.toArray(pArgTypes);
+ long func = Native.mkFuncDecl(environment, symbol, sorts.length, sorts, returnType);
+ Native.incRef(environment, func);
+ symbolsToDeclarations.put(pName, func);
+ return func;
+ }
+
+ @Override
+ public Long callFunctionImpl(Long declaration, List args) {
+ return Native.mkApp(environment, declaration, args.size(), Longs.toArray(args));
+ }
+
+ @Override
+ protected Long getBooleanVarDeclarationImpl(Long pLong) {
+ return Native.getAppDecl(getEnv(), pLong);
+ }
+
+ /** returns, if the function of the expression is the given operation. */
+ static boolean isOP(long z3context, long expr, Z3_decl_kind op) {
+ if (!Native.isApp(z3context, expr)) {
+ return false;
+ }
+
+ long decl = Native.getAppDecl(z3context, expr);
+ return Native.getDeclKind(z3context, decl) == op.toInt();
+ }
+
+ /**
+ * Apply multiple tactics in sequence.
+ *
+ * @throws InterruptedException thrown by JNI code in case of termination request
+ * @throws SolverException thrown by JNI code in case of error
+ */
+ public long applyTactics(long z3context, final Long pF, String... pTactics)
+ throws InterruptedException, SolverException {
+ long overallResult = pF;
+ for (String tactic : pTactics) {
+ overallResult = applyTactic(z3context, overallResult, tactic);
+ }
+ return overallResult;
+ }
+
+ /**
+ * Apply tactic on a Z3_ast object, convert the result back to Z3_ast.
+ *
+ * @param z3context Z3_context
+ * @param tactic Z3 Tactic Name
+ * @param pF Z3_ast
+ * @return Z3_ast
+ * @throws InterruptedException If execution gets interrupted.
+ */
+ public long applyTactic(long z3context, long pF, String tactic)
+ throws InterruptedException, SolverException {
+ long tacticObject = Native.mkTactic(z3context, tactic);
+ Native.tacticIncRef(z3context, tacticObject);
+
+ long goal = Native.mkGoal(z3context, true, false, false);
+ Native.goalIncRef(z3context, goal);
+ Native.goalAssert(z3context, goal, pF);
+
+ long result;
+ try {
+ result = Native.tacticApply(z3context, tacticObject, goal);
+ } catch (Z3Exception exp) {
+ throw handleZ3Exception(exp);
+ }
+
+ try {
+ return applyResultToAST(z3context, result);
+ } finally {
+ Native.goalDecRef(z3context, goal);
+ Native.tacticDecRef(z3context, tacticObject);
+ }
+ }
+
+ private long applyResultToAST(long z3context, long applyResult) {
+ int subgoalsCount = Native.applyResultGetNumSubgoals(z3context, applyResult);
+ long[] goalFormulas = new long[subgoalsCount];
+ for (int i = 0; i < subgoalsCount; i++) {
+ long subgoal = Native.applyResultGetSubgoal(z3context, applyResult, i);
+ goalFormulas[i] = goalToAST(z3context, subgoal);
+ }
+ return goalFormulas.length == 1
+ ? goalFormulas[0]
+ : Native.mkOr(z3context, goalFormulas.length, goalFormulas);
+ }
+
+ private long goalToAST(long z3context, long goal) {
+ int subgoalFormulasCount = Native.goalSize(z3context, goal);
+ long[] subgoalFormulas = new long[subgoalFormulasCount];
+ for (int k = 0; k < subgoalFormulasCount; k++) {
+ subgoalFormulas[k] = Native.goalFormula(z3context, goal, k);
+ }
+ return subgoalFormulas.length == 1
+ ? subgoalFormulas[0]
+ : Native.mkAnd(z3context, subgoalFormulas.length, subgoalFormulas);
+ }
+
+ /** Closing the context. */
+ @SuppressWarnings("empty-statement")
+ public void forceClose() {
+ // Force clean all ASTs, even those which were not GC'd yet.
+ if (usePhantomReferences) {
+ Z3AstReference cur = referenceListHead.next;
+ assert cur != null;
+ while (cur.next != null) {
+ Native.decRef(environment, cur.z3Ast);
+ cur = cur.next;
+ }
+ Z3AstReference tail = cur;
+ // Bulk delete everything between head and tail
+ referenceListHead.next = tail;
+ tail.prev = referenceListHead;
+
+ // Remove already enqueued references.
+ while (referenceQueue.poll() != null) {
+ // NOTE: Together with the above list deletion, this empty loop will guarantee that no more
+ // ast references are reachable by the GC making them all eligible for garbage collection
+ // and preventing them from getting enqueued into the reference queue in the future.
+ }
+ }
+ }
+
+ /**
+ * get a previously created application declaration, or NULL if the symbol is
+ * unknown.
+ */
+ @Nullable Long getKnownDeclaration(String symbolName) {
+ return symbolsToDeclarations.get(symbolName);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaManager.java
new file mode 100644
index 0000000000..e71c495e25
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaManager.java
@@ -0,0 +1,245 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.z3legacy;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
+import com.google.common.primitives.Longs;
+import com.microsoft.z3legacy.Native;
+import com.microsoft.z3legacy.Z3Exception;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
+
+final class Z3LegacyFormulaManager extends AbstractFormulaManager {
+
+ private final Z3LegacyFormulaCreator formulaCreator;
+
+ @SuppressWarnings("checkstyle:parameternumber")
+ Z3LegacyFormulaManager(
+ Z3LegacyFormulaCreator pFormulaCreator,
+ Z3LegacyUFManager pFunctionManager,
+ Z3LegacyBooleanFormulaManager pBooleanManager,
+ Z3LegacyIntegerFormulaManager pIntegerManager,
+ Z3LegacyRationalFormulaManager pRationalManager,
+ Z3LegacyBitvectorFormulaManager pBitpreciseManager,
+ Z3LegacyFloatingPointFormulaManager pFloatingPointManager,
+ Z3LegacyQuantifiedFormulaManager pQuantifiedManager,
+ Z3LegacyArrayFormulaManager pArrayManager,
+ Z3LegacyStringFormulaManager pStringManager,
+ Z3LegacyEnumerationFormulaManager pEnumerationManager) {
+ super(
+ pFormulaCreator,
+ pFunctionManager,
+ pBooleanManager,
+ pIntegerManager,
+ pRationalManager,
+ pBitpreciseManager,
+ pFloatingPointManager,
+ pQuantifiedManager,
+ pArrayManager,
+ null,
+ pStringManager,
+ pEnumerationManager);
+ formulaCreator = pFormulaCreator;
+ }
+
+ @Override
+ public Long parseImpl(String str) throws IllegalArgumentException {
+
+ // Z3 does not access the existing symbols on its own,
+ // but requires all symbols as part of the query.
+ // Thus, we track the used symbols on our own and give them to the parser call, if required.
+ // Later, we collect all symbols from the parsed query and
+ // define them again to have them tracked.
+
+ final long env = getEnvironment();
+
+ // JavaSMT does currently not allow defining new sorts, future work?
+ long[] sortSymbols = new long[0];
+ long[] sorts = new long[0];
+
+ // first step: lets try to parse the query directly, without additional information
+ List declSymbols = new ArrayList<>();
+ List decls = new ArrayList<>();
+
+ long e = 0;
+ boolean finished = false;
+ while (!finished) {
+ try {
+ e =
+ Native.parseSmtlib2String(
+ env,
+ str,
+ sorts.length,
+ sortSymbols,
+ sorts,
+ declSymbols.size(),
+ Longs.toArray(declSymbols),
+ Longs.toArray(decls));
+ finished = true;
+
+ } catch (Z3Exception nested) {
+ // get the missing symbol and restart the parsing with them
+ Pattern pattern =
+ Pattern.compile(
+ "\\(error \"line \\d+ column \\d+: unknown constant"
+ + " (?.*?)\\s?(?\\(.*\\))?\\s?\\\"\\)\\n");
+ Matcher matcher = pattern.matcher(nested.getMessage());
+ if (matcher.matches()) {
+ String missingSymbol = matcher.group(1);
+ Long appDecl = formulaCreator.getKnownDeclaration(missingSymbol);
+ if (appDecl != null) { // if the symbol is known, then use it
+ declSymbols.add(Native.mkStringSymbol(env, missingSymbol));
+ decls.add(appDecl);
+ continue; // restart the parsing
+ }
+ }
+ throw new IllegalArgumentException(nested);
+ }
+ }
+
+ Preconditions.checkState(e != 0, "parsing aborted");
+ final int size = Native.astVectorSize(env, e);
+ Preconditions.checkState(
+ size == 1, "parsing expects exactly one asserted term, but got %s terms", size);
+ final long term = Native.astVectorGet(env, e, 0);
+
+ // last step: all parsed symbols need to be declared again to have them tracked in the creator.
+ declareAllSymbols(term);
+
+ return term;
+ }
+
+ @SuppressWarnings("CheckReturnValue")
+ private void declareAllSymbols(final long term) {
+ final long env = getEnvironment();
+ final Map symbols = formulaCreator.extractVariablesAndUFs(term, true);
+ for (Map.Entry symbol : symbols.entrySet()) {
+ long sym = symbol.getValue();
+ String name = symbol.getKey();
+ assert Native.isApp(env, sym);
+ int arity = Native.getAppNumArgs(env, sym);
+ if (arity == 0) { // constants
+ formulaCreator.makeVariable(Native.getSort(env, sym), name);
+ } else {
+ ImmutableList.Builder argTypes = ImmutableList.builder();
+ for (int j = 0; j < arity; j++) {
+ argTypes.add(Native.getSort(env, Native.getAppArg(env, sym, j)));
+ }
+ formulaCreator.declareUFImpl(name, Native.getSort(env, sym), argTypes.build());
+ }
+ }
+ }
+
+ @Override
+ protected BooleanFormula applyQELightImpl(BooleanFormula pF)
+ throws InterruptedException, SolverException {
+ return applyTacticImpl(pF, "qe-light");
+ }
+
+ @Override
+ protected BooleanFormula applyCNFImpl(BooleanFormula pF)
+ throws InterruptedException, SolverException {
+ return applyTacticImpl(pF, "tseitin-cnf");
+ }
+
+ @Override
+ protected BooleanFormula applyNNFImpl(BooleanFormula pF)
+ throws InterruptedException, SolverException {
+ return applyTacticImpl(pF, "nnf");
+ }
+
+ private BooleanFormula applyTacticImpl(BooleanFormula pF, String tacticName)
+ throws InterruptedException, SolverException {
+ long out =
+ formulaCreator.applyTactic(getFormulaCreator().getEnv(), extractInfo(pF), tacticName);
+ return formulaCreator.encapsulateBoolean(out);
+ }
+
+ @Override
+ public String dumpFormulaImpl(final Long expr) {
+ assert getFormulaCreator().getFormulaType(expr) == FormulaType.BooleanType
+ : "Only BooleanFormulas may be dumped";
+
+ // Serializing a solver is the simplest way to dump a formula in Z3,
+ // cf https://github.com/Z3Prover/z3/issues/397
+ long z3solver = Native.mkSolver(getEnvironment());
+ Native.solverIncRef(getEnvironment(), z3solver);
+ Native.solverAssert(getEnvironment(), z3solver, expr);
+ String serialized = Native.solverToString(getEnvironment(), z3solver);
+ Native.solverDecRef(getEnvironment(), z3solver);
+ return serialized;
+ }
+
+ @Override
+ protected Long simplify(Long pF) throws InterruptedException {
+ try {
+ try {
+ return Native.simplify(getFormulaCreator().getEnv(), pF);
+ } catch (Z3Exception exp) {
+ throw formulaCreator.handleZ3Exception(exp);
+ }
+ } catch (SolverException e) {
+ // ignore exception and return original formula AS-IS.
+ return pF;
+ }
+ }
+
+ @Override
+ public T substitute(
+ final T f, final Map fromToMapping) {
+ long[] changeFrom = new long[fromToMapping.size()];
+ long[] changeTo = new long[fromToMapping.size()];
+ int idx = 0;
+ for (Map.Entry e : fromToMapping.entrySet()) {
+ changeFrom[idx] = extractInfo(e.getKey());
+ changeTo[idx] = extractInfo(e.getValue());
+ idx++;
+ }
+ FormulaType type = getFormulaType(f);
+ return getFormulaCreator()
+ .encapsulate(
+ type,
+ Native.substitute(
+ getFormulaCreator().getEnv(),
+ extractInfo(f),
+ fromToMapping.size(),
+ changeFrom,
+ changeTo));
+ }
+
+ @Override
+ public BooleanFormula translateFrom(BooleanFormula other, FormulaManager otherManager) {
+ if (otherManager instanceof Z3LegacyFormulaManager) {
+ long otherZ3Context = ((Z3LegacyFormulaManager) otherManager).getEnvironment();
+ if (otherZ3Context == getEnvironment()) {
+
+ // Same context.
+ return other;
+ } else {
+
+ // Z3-to-Z3 translation.
+ long translatedAST = Native.translate(otherZ3Context, extractInfo(other), getEnvironment());
+ return getFormulaCreator().encapsulateBoolean(translatedAST);
+ }
+ }
+ return super.translateFrom(other, otherManager);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyIntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyIntegerFormulaManager.java
new file mode 100644
index 0000000000..af0de67f37
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyIntegerFormulaManager.java
@@ -0,0 +1,86 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.z3legacy;
+
+import com.microsoft.z3legacy.Native;
+import java.math.BigDecimal;
+import java.math.BigInteger;
+import org.sosy_lab.java_smt.api.IntegerFormulaManager;
+import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+
+class Z3LegacyIntegerFormulaManager
+ extends Z3LegacyNumeralFormulaManager
+ implements IntegerFormulaManager {
+
+ Z3LegacyIntegerFormulaManager(
+ Z3LegacyFormulaCreator pCreator, NonLinearArithmetic pNonLinearArithmetic) {
+ super(pCreator, pNonLinearArithmetic);
+ }
+
+ @Override
+ protected long getNumeralType() {
+ return getFormulaCreator().getIntegerType();
+ }
+
+ @Override
+ protected Long makeNumberImpl(double pNumber) {
+ return makeNumberImpl((long) pNumber);
+ }
+
+ @Override
+ protected Long makeNumberImpl(BigDecimal pNumber) {
+ return decimalAsInteger(pNumber);
+ }
+
+ @Override
+ public Long modulo(Long pNumber1, Long pNumber2) {
+ return Native.mkMod(z3context, pNumber1, pNumber2);
+ }
+
+ @Override
+ protected Long modularCongruence(Long pNumber1, Long pNumber2, long pModulo) {
+ long n = makeNumberImpl(pModulo);
+ Native.incRef(z3context, n);
+ try {
+ return modularCongruence0(pNumber1, pNumber2, makeNumberImpl(pModulo));
+ } finally {
+ Native.decRef(z3context, n);
+ }
+ }
+
+ @Override
+ protected Long modularCongruence(Long pNumber1, Long pNumber2, BigInteger pModulo) {
+ long n = makeNumberImpl(pModulo);
+ Native.incRef(z3context, n);
+ try {
+ return modularCongruence0(pNumber1, pNumber2, makeNumberImpl(pModulo));
+ } finally {
+ Native.decRef(z3context, n);
+ }
+ }
+
+ protected Long modularCongruence0(Long pNumber1, Long pNumber2, Long n) {
+ // ((_ divisible n) x) <==> (= x (* n (div x n)))
+ long x = subtract(pNumber1, pNumber2);
+ Native.incRef(z3context, x);
+ long div = Native.mkDiv(z3context, x, n);
+ Native.incRef(z3context, div);
+ long mul = Native.mkMul(z3context, 2, new long[] {n, div});
+ Native.incRef(z3context, mul);
+ try {
+ return Native.mkEq(z3context, x, mul);
+ } finally {
+ Native.decRef(z3context, x);
+ Native.decRef(z3context, div);
+ Native.decRef(z3context, mul);
+ }
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyInterpolatingProver.java
new file mode 100644
index 0000000000..c27b899347
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyInterpolatingProver.java
@@ -0,0 +1,263 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.z3legacy;
+
+import static com.google.common.base.Preconditions.checkArgument;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.Iterables;
+import com.google.common.primitives.Longs;
+import com.microsoft.z3legacy.Native;
+import com.microsoft.z3legacy.Z3Exception;
+import java.util.ArrayDeque;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Deque;
+import java.util.List;
+import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.common.io.PathCounterTemplate;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
+import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
+import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor;
+import org.sosy_lab.java_smt.api.visitors.TraversalProcess;
+
+class Z3LegacyInterpolatingProver extends Z3LegacyAbstractProver
+ implements InterpolatingProverEnvironment {
+
+ Z3LegacyInterpolatingProver(
+ Z3LegacyFormulaCreator pCreator,
+ Z3LegacyFormulaManager pMgr,
+ Set pOptions,
+ @Nullable PathCounterTemplate pLogfile,
+ ShutdownNotifier pShutdownNotifier) {
+ super(pCreator, pMgr, pOptions, pLogfile, pShutdownNotifier);
+ }
+
+ @Override
+ @SuppressWarnings({"unchecked", "varargs"})
+ public BooleanFormula getInterpolant(final Collection pFormulasOfA)
+ throws InterruptedException, SolverException {
+ Preconditions.checkState(!closed);
+ checkArgument(
+ getAssertedConstraintIds().containsAll(pFormulasOfA),
+ "interpolation can only be done over previously asserted formulas.");
+
+ Set formulasOfA = ImmutableSet.copyOf(pFormulasOfA);
+
+ // calc difference: formulasOfB := assertedFormulas - formulasOfA
+ Set formulasOfB =
+ getAssertedConstraintIds().stream()
+ .filter(f -> !formulasOfA.contains(f))
+ .collect(ImmutableSet.toImmutableSet());
+
+ // binary interpolant is a sequence interpolant of only 2 elements
+ return Iterables.getOnlyElement(getSeqInterpolants(ImmutableList.of(formulasOfA, formulasOfB)));
+ }
+
+ @Override
+ public List getTreeInterpolants(
+ List> partitionedFormulas, int[] startOfSubTree)
+ throws InterruptedException, SolverException {
+ Preconditions.checkState(!closed);
+ assert InterpolatingProverEnvironment.checkTreeStructure(
+ partitionedFormulas.size(), startOfSubTree);
+
+ final long[] conjunctionFormulas = buildConjunctions(partitionedFormulas);
+ final long[] interpolationFormulas =
+ buildFormulaTree(partitionedFormulas, startOfSubTree, conjunctionFormulas);
+ final long root = interpolationFormulas[interpolationFormulas.length - 1];
+
+ final long proof = Native.solverGetProof(z3context, z3solver);
+ Native.incRef(z3context, proof);
+
+ final long interpolationResult = computeInterpolants(root, proof);
+
+ // n partitions -> n-1 interpolants
+ // the given tree interpolants are sorted in post-order,
+ // so we only need to copy them
+ final List result = new ArrayList<>();
+ for (int i = 0; i < partitionedFormulas.size() - 1; i++) {
+ result.add(
+ creator.encapsulateBoolean(Native.astVectorGet(z3context, interpolationResult, i)));
+ }
+ assert result.size() == startOfSubTree.length - 1;
+
+ // cleanup
+ Native.decRef(z3context, proof);
+ for (long partition : conjunctionFormulas) {
+ Native.decRef(z3context, partition);
+ }
+ for (long partition : interpolationFormulas) {
+ Native.decRef(z3context, partition);
+ }
+
+ checkInterpolantsForUnboundVariables(result); // Do this last after cleanup.
+
+ return result;
+ }
+
+ /** build a conjunction of each partition. */
+ private long[] buildConjunctions(List> partitionedFormulas) {
+ final long[] conjunctionFormulas = new long[partitionedFormulas.size()];
+ for (int i = 0; i < partitionedFormulas.size(); i++) {
+ long conjunction =
+ Native.mkAnd(
+ z3context,
+ partitionedFormulas.get(i).size(),
+ Longs.toArray(partitionedFormulas.get(i)));
+ Native.incRef(z3context, conjunction);
+ conjunctionFormulas[i] = conjunction;
+ }
+ return conjunctionFormulas;
+ }
+
+ /** build tree of interpolation-points. */
+ private long[] buildFormulaTree(
+ List> partitionedFormulas,
+ int[] startOfSubTree,
+ final long[] conjunctionFormulas) {
+ final long[] interpolationFormulas = new long[partitionedFormulas.size()];
+ final Deque stack = new ArrayDeque<>();
+
+ int lastSubtree = -1; // subtree starts with 0. With -1<0 we start a new subtree.
+ for (int i = 0; i < startOfSubTree.length; i++) {
+ final int currentSubtree = startOfSubTree[i];
+ final long conjunction;
+ if (currentSubtree > lastSubtree) {
+ // start of a new subtree -> first element has no children
+ conjunction = conjunctionFormulas[i];
+
+ } else { // if (currentSubtree <= lastSubtree) {
+ // merge-point in tree, several children at a node -> pop from stack and conjunct
+ final Deque children = new ArrayDeque<>();
+ while (!stack.isEmpty() && currentSubtree <= stack.peek().getRootOfTree()) {
+ // adding at front is important for tree-structure!
+ children.addFirst(stack.pop().getInterpolationPoint());
+ }
+ children.add(conjunctionFormulas[i]); // add the node itself
+ conjunction = Native.mkAnd(z3context, children.size(), Longs.toArray(children));
+ }
+
+ final long interpolationPoint;
+ if (i == startOfSubTree.length - 1) {
+ // the last node in the tree (=root) does not need the interpolation-point-flag
+ interpolationPoint = conjunction;
+ Preconditions.checkState(currentSubtree == 0, "subtree of root should start at 0.");
+ Preconditions.checkState(stack.isEmpty(), "root should be the last element in the stack.");
+ } else {
+ interpolationPoint = Native.mkInterpolant(z3context, conjunction);
+ }
+
+ Native.incRef(z3context, interpolationPoint);
+ interpolationFormulas[i] = interpolationPoint;
+ stack.push(new Z3TreeInterpolant(currentSubtree, interpolationPoint));
+ lastSubtree = currentSubtree;
+ }
+
+ Preconditions.checkState(
+ stack.peek().getRootOfTree() == 0, "subtree of root should start at 0.");
+ long root = stack.pop().getInterpolationPoint();
+ Preconditions.checkState(
+ root == interpolationFormulas[interpolationFormulas.length - 1],
+ "subtree of root should start at 0.");
+ Preconditions.checkState(
+ stack.isEmpty(), "root should have been the last element in the stack.");
+
+ return interpolationFormulas;
+ }
+
+ /** compute interpolants for the given tree of formulas and dump the interpolation problem. */
+ private long computeInterpolants(final long root, final long proof)
+ throws SolverException, InterruptedException {
+ long interpolationResult;
+ try {
+ interpolationResult =
+ Native.getInterpolant(
+ z3context,
+ proof, // refutation of premises := proof
+ root, // last element is end of chain (root of tree), pattern := interpolation tree
+ Native.mkParams(z3context));
+ } catch (Z3Exception e) {
+ if ("theory not supported by interpolation or bad proof".equals(e.getMessage())) {
+ throw new SolverException(e.getMessage(), e);
+ }
+ throw creator.handleZ3Exception(e);
+ }
+ return interpolationResult;
+ }
+
+ /**
+ * Check whether any formula in a given list contains unbound variables. Z3 has the problem that
+ * it sometimes returns such invalid formulas as interpolants
+ * (https://github.com/Z3Prover/z3/issues/665).
+ */
+ @SuppressWarnings("deprecation")
+ private void checkInterpolantsForUnboundVariables(List itps)
+ throws SolverException {
+ List unboundVariables = new ArrayList<>(1);
+ final DefaultFormulaVisitor unboundVariablesCollector =
+ new DefaultFormulaVisitor() {
+ @Override
+ public TraversalProcess visitBoundVariable(Formula f, int deBruijnIdx) {
+ unboundVariables.add(f);
+ return TraversalProcess.ABORT;
+ }
+
+ @Override
+ public TraversalProcess visitQuantifier(
+ BooleanFormula pF,
+ Quantifier pQ,
+ List pBoundVariables,
+ BooleanFormula pBody) {
+ return TraversalProcess.SKIP; // bound variables in quantifiers are probably ok
+ }
+
+ @Override
+ protected TraversalProcess visitDefault(org.sosy_lab.java_smt.api.Formula pF) {
+ return TraversalProcess.CONTINUE;
+ }
+ };
+
+ for (BooleanFormula itp : itps) {
+ creator.visitRecursively(unboundVariablesCollector, itp);
+ if (!unboundVariables.isEmpty()) {
+ throw new SolverException(
+ "Unbound variable " + unboundVariables.get(0) + " in interpolant " + itp);
+ }
+ }
+ }
+
+ private static class Z3TreeInterpolant {
+ private final int rootOfSubTree;
+ private final long interpolationPoint;
+
+ private Z3TreeInterpolant(int pRootOfSubtree, long pInterpolationPoint) {
+ rootOfSubTree = pRootOfSubtree;
+ interpolationPoint = pInterpolationPoint;
+ }
+
+ private int getRootOfTree() {
+ return rootOfSubTree;
+ }
+
+ private long getInterpolationPoint() {
+ return interpolationPoint;
+ }
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyModel.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyModel.java
new file mode 100644
index 0000000000..1b556b12a1
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyModel.java
@@ -0,0 +1,405 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.z3legacy;
+
+import com.google.common.base.Preconditions;
+import com.google.common.base.VerifyException;
+import com.google.common.collect.ImmutableList;
+import com.microsoft.z3legacy.Native;
+import com.microsoft.z3legacy.Native.LongPtr;
+import com.microsoft.z3legacy.Z3Exception;
+import com.microsoft.z3legacy.enumerations.Z3_decl_kind;
+import com.microsoft.z3legacy.enumerations.Z3_sort_kind;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+import java.util.regex.Pattern;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.java_smt.basicimpl.AbstractModel;
+import org.sosy_lab.java_smt.basicimpl.AbstractProver;
+
+final class Z3LegacyModel extends AbstractModel {
+
+ private final long model;
+ private final long z3context;
+ private static final Pattern Z3_IRRELEVANT_MODEL_TERM_PATTERN = Pattern.compile(".*![0-9]+");
+
+ private final Z3LegacyFormulaCreator z3creator;
+
+ Z3LegacyModel(
+ AbstractProver pProver, long z3context, long z3model, Z3LegacyFormulaCreator pCreator) {
+ super(pProver, pCreator);
+ Native.modelIncRef(z3context, z3model);
+ model = z3model;
+ this.z3context = z3context;
+ z3creator = pCreator;
+ }
+
+ @Override
+ public ImmutableList asList() {
+ Preconditions.checkState(!isClosed());
+ ImmutableList.Builder out = ImmutableList.builder();
+
+ try {
+ // Iterate through constants.
+ for (int constIdx = 0; constIdx < Native.modelGetNumConsts(z3context, model); constIdx++) {
+ long keyDecl = Native.modelGetConstDecl(z3context, model, constIdx);
+ Native.incRef(z3context, keyDecl);
+ out.addAll(getConstAssignments(keyDecl));
+ Native.decRef(z3context, keyDecl);
+ }
+
+ // Iterate through function applications.
+ for (int funcIdx = 0; funcIdx < Native.modelGetNumFuncs(z3context, model); funcIdx++) {
+ long funcDecl = Native.modelGetFuncDecl(z3context, model, funcIdx);
+ Native.incRef(z3context, funcDecl);
+ if (!isInternalSymbol(funcDecl)) {
+ String functionName = z3creator.symbolToString(Native.getDeclName(z3context, funcDecl));
+ out.addAll(getFunctionAssignments(funcDecl, funcDecl, functionName));
+ }
+ Native.decRef(z3context, funcDecl);
+ }
+ } catch (Z3Exception e) {
+ throw z3creator.handleZ3ExceptionAsRuntimeException(e);
+ }
+
+ return out.build();
+ }
+
+ /**
+ * The symbol "!" is part of temporary symbols used for quantified formulas or aliases. This
+ * method is only a heuristic, because the user can also create a symbol containing "!".
+ */
+ private boolean isInternalSymbol(long funcDecl) {
+ switch (Z3_decl_kind.fromInt(Native.getDeclKind(z3context, funcDecl))) {
+ case Z3_OP_SELECT:
+ case Z3_OP_ARRAY_EXT:
+ return true;
+ default:
+ return Z3_IRRELEVANT_MODEL_TERM_PATTERN
+ .matcher(z3creator.symbolToString(Native.getDeclName(z3context, funcDecl)))
+ .matches();
+ }
+ }
+
+ /**
+ * @return ValueAssignments for a constant declaration in the model
+ */
+ private Collection getConstAssignments(long keyDecl) {
+ Preconditions.checkArgument(
+ Native.getArity(z3context, keyDecl) == 0, "Declaration is not a constant");
+
+ long var = Native.mkApp(z3context, keyDecl, 0, new long[] {});
+ long value = Native.modelGetConstInterp(z3context, model, keyDecl);
+ checkReturnValue(value, keyDecl);
+ Native.incRef(z3context, value);
+
+ long equality = Native.mkEq(z3context, var, value);
+ Native.incRef(z3context, equality);
+
+ try {
+ long symbol = Native.getDeclName(z3context, keyDecl);
+ if (z3creator.isConstant(value)) {
+ return ImmutableList.of(
+ new ValueAssignment(
+ z3creator.encapsulateWithTypeOf(var),
+ z3creator.encapsulateWithTypeOf(value),
+ z3creator.encapsulateBoolean(equality),
+ z3creator.symbolToString(symbol),
+ z3creator.convertValue(value),
+ ImmutableList.of()));
+
+ } else if (Native.isAsArray(z3context, value)) {
+ long arrayFormula = Native.mkConst(z3context, symbol, Native.getSort(z3context, value));
+ Native.incRef(z3context, arrayFormula);
+ return getArrayAssignments(symbol, arrayFormula, value, ImmutableList.of());
+
+ } else if (Native.isApp(z3context, value)) {
+ long decl = Native.getAppDecl(z3context, value);
+ Native.incRef(z3context, decl);
+ Z3_sort_kind sortKind =
+ Z3_sort_kind.fromInt(Native.getSortKind(z3context, Native.getSort(z3context, value)));
+ assert sortKind == Z3_sort_kind.Z3_ARRAY_SORT : "unexpected sort: " + sortKind;
+
+ try {
+ return getConstantArrayAssignment(symbol, value, decl);
+ } finally {
+ Native.decRef(z3context, decl);
+ }
+ }
+
+ throw new UnsupportedOperationException(
+ "unknown model evaluation: " + Native.astToString(z3context, value));
+
+ } finally {
+ // cleanup outdated data
+ Native.decRef(z3context, value);
+ }
+ }
+
+ /** unrolls an constant array assignment. */
+ private Collection getConstantArrayAssignment(
+ long arraySymbol, long value, long decl) {
+
+ long arrayFormula = Native.mkConst(z3context, arraySymbol, Native.getSort(z3context, value));
+ Native.incRef(z3context, arrayFormula);
+
+ Z3_decl_kind declKind = Z3_decl_kind.fromInt(Native.getDeclKind(z3context, decl));
+ int numArgs = Native.getAppNumArgs(z3context, value);
+
+ List out = new ArrayList<>();
+
+ // avoid doubled ValueAssignments for cases like "(store (store ARR 0 0) 0 1)",
+ // where we could (but should not!) unroll the array into "[ARR[0]=1, ARR[0]=1]"
+ Set indizes = new HashSet<>();
+
+ // unroll an array...
+ while (Z3_decl_kind.Z3_OP_STORE == declKind) {
+ assert numArgs == 3;
+
+ long arrayIndex = Native.getAppArg(z3context, value, 1);
+ Native.incRef(z3context, arrayIndex);
+
+ if (indizes.add(arrayIndex)) {
+ long select = Native.mkSelect(z3context, arrayFormula, arrayIndex);
+ Native.incRef(z3context, select);
+
+ long nestedValue = Native.getAppArg(z3context, value, 2);
+ Native.incRef(z3context, nestedValue);
+
+ long equality = Native.mkEq(z3context, select, nestedValue);
+ Native.incRef(z3context, equality);
+
+ out.add(
+ new ValueAssignment(
+ z3creator.encapsulateWithTypeOf(select),
+ z3creator.encapsulateWithTypeOf(nestedValue),
+ z3creator.encapsulateBoolean(equality),
+ z3creator.symbolToString(arraySymbol),
+ z3creator.convertValue(nestedValue),
+ ImmutableList.of(evaluateImpl(arrayIndex))));
+ }
+
+ Native.decRef(z3context, arrayIndex);
+
+ // recursive unrolling
+ value = Native.getAppArg(z3context, value, 0);
+ decl = Native.getAppDecl(z3context, value);
+ declKind = Z3_decl_kind.fromInt(Native.getDeclKind(z3context, decl));
+ numArgs = Native.getAppNumArgs(z3context, value);
+ }
+
+ // ...until its end
+ if (Z3_decl_kind.Z3_OP_CONST_ARRAY == declKind) {
+ assert numArgs == 1;
+ // We have an array of zeros (=default value) as "((as const (Array Int Int)) 0)".
+ // There is no way of modeling a whole array, thus we ignore it.
+ }
+
+ return out;
+ }
+
+ /**
+ * Z3 models an array as an uninterpreted function.
+ *
+ * @return a list of assignments {@code a[1]=0; a[2]=0; a[5]=0}.
+ */
+ private Collection getArrayAssignments(
+ long arraySymbol, long arrayFormula, long value, List | |