- implemented support for BITWUZLA in Benchmark

DavidGalllob · DavidGalllob · commit f2d4b800ad14 · 2025-04-03T19:34:15.000+02:00
diff --git a/src/org/sosy_lab/java_smt/utils/ParseGenerateAndReparse.java b/src/org/sosy_lab/java_smt/utils/ParseGenerateAndReparse.java
@@ -120,6 +120,7 @@ public static boolean checkNativeParseAndIsUnsat(Solvers solver, String smt2)
     switch (solver){
       case Z3: return nativeZ3ParseAndIsUnsat(smt2);
       case MATHSAT5: return nativeMathSatParseAndIsUnsat(smt2);
+      case BITWUZLA: return nativeBitwuzlaParseAndIsUnsat(smt2);
     }
     throw new SolverException("Unsupported solver: " + solver);
   }
@@ -132,6 +133,13 @@ public static boolean nativeZ3ParseAndIsUnsat(String smt2) {
       return status == Status.UNSATISFIABLE;
     }
   }
+  public static boolean nativeBitwuzlaParseAndIsUnsat(String smt2)
+      throws InvalidConfigurationException, InterruptedException, SolverException {
+    SolverContext bitwuz = SolverContextFactory.createSolverContext(Solvers.BITWUZLA);
+    ProverEnvironment prover = bitwuz.newProverEnvironment(ProverOptions.GENERATE_MODELS);
+    prover.addConstraint(bitwuz.getFormulaManager().parse(smt2));
+    return prover.isUnsat();
+  }
 
   public static boolean nativeMathSatParseAndIsUnsat(String smt2)
       throws InvalidConfigurationException, InterruptedException, SolverException {

Original file line number	Diff line number	Diff line change
`@@ -120,6 +120,7 @@ public static boolean checkNativeParseAndIsUnsat(Solvers solver, String smt2)`
`120`	`120`	`switch (solver){`
`121`	`121`	`case Z3: return nativeZ3ParseAndIsUnsat(smt2);`
`122`	`122`	`case MATHSAT5: return nativeMathSatParseAndIsUnsat(smt2);`
	`123`	`+ case BITWUZLA: return nativeBitwuzlaParseAndIsUnsat(smt2);`
`123`	`124`	`}`
`124`	`125`	`throw new SolverException("Unsupported solver: " + solver);`
`125`	`126`	`}`
`@@ -132,6 +133,13 @@ public static boolean nativeZ3ParseAndIsUnsat(String smt2) {`
`132`	`133`	`return status == Status.UNSATISFIABLE;`
`133`	`134`	`}`
`134`	`135`	`}`
	`136`	`+ public static boolean nativeBitwuzlaParseAndIsUnsat(String smt2)`
	`137`	`+ throws InvalidConfigurationException, InterruptedException, SolverException {`
	`138`	`+ SolverContext bitwuz = SolverContextFactory.createSolverContext(Solvers.BITWUZLA);`
	`139`	`+ ProverEnvironment prover = bitwuz.newProverEnvironment(ProverOptions.GENERATE_MODELS);`
	`140`	`+ prover.addConstraint(bitwuz.getFormulaManager().parse(smt2));`
	`141`	`+ return prover.isUnsat();`
	`142`	`+ }`
`135`	`143`
`136`	`144`	`public static boolean nativeMathSatParseAndIsUnsat(String smt2)`
`137`	`145`	`throws InvalidConfigurationException, InterruptedException, SolverException {`