option : furtherOptionsMap.entrySet()) {
+ String optionName = option.getKey();
+ String optionValue = option.getValue();
+ Option bitwuzlaOption = getBitwuzlaOptByString(optionName);
+ try {
+ if (pOptions.is_numeric(bitwuzlaOption)) {
+ pOptions.set(bitwuzlaOption, Integer.parseInt(optionValue));
+ } else {
+ pOptions.set(bitwuzlaOption, option.getValue());
+ }
+ } catch (NumberFormatException e) {
+ throw new InvalidConfigurationException(
+ "Option "
+ + bitwuzlaOption
+ + " needs a numeric "
+ + "value as option value, but you entered "
+ + optionValue);
+ }
+ }
+ return pOptions;
+ }
+
+ private static Options buildBitwuzlaOptions(BitwuzlaSettings settings, long randomSeed)
+ throws InvalidConfigurationException {
+ Preconditions.checkNotNull(settings.getSatSolver());
+
+ Options options = new Options();
+ options.set(SAT_SOLVER, settings.getSatSolver().name().toLowerCase(Locale.getDefault()));
+ options.set(SEED, (int) randomSeed);
+ options.set(REWRITE_LEVEL, 0); // Stop Bitwuzla from rewriting formulas in outputs
+
+ return setFurtherOptions(options, settings.getFurtherOptions());
+ }
+
+ /**
+ * Get version information out of the solver.
+ *
+ * In most cases, the version contains the name of the solver followed by some numbers and
+ * additional info about the version, e.g., "SMTInterpol 2.5-12-g3d15a15c".
+ */
+ @Override
+ public String getVersion() {
+ return "Bitwuzla " + BitwuzlaNative.version();
+ }
+
+ /**
+ * Get solver name (MATHSAT5/Z3/etc...).
+ *
+ *
This is an uppercase String matching the enum identifier from {@link Solvers}
+ */
+ @Override
+ public Solvers getSolverName() {
+ return Solvers.BITWUZLA;
+ }
+
+ /**
+ * Close the solver context.
+ *
+ *
After calling this method, further access to any object that had been returned from this
+ * context is not wanted, i.e., it depends on the solver. Java-based solvers might wait for the
+ * next garbage collection with any cleanup operation. Native solvers might even reference invalid
+ * memory and cause segmentation faults.
+ *
+ *
Necessary for the solvers implemented in native code, frees the associated memory.
+ */
+ @Override
+ public void close() {
+ if (!closed) {
+ creator.getTermManager().delete();
+ closed = true;
+ }
+ }
+
+ @Override
+ protected ProverEnvironment newProverEnvironment0(Set