Skip to content

Commit 9167122

Browse files
DavidGalllobDavidGalllob
committed
- Benchmark now only supports Z3
1 parent 785ccd1 commit 9167122

File tree

5 files changed

+35
-148
lines changed

5 files changed

+35
-148
lines changed

‎src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -78,8 +78,9 @@ public BooleanFormula equal(StringFormula str1, StringFormula str2) {
7878
public BooleanFormula greaterThan(StringFormula str1, StringFormula str2) {
7979
BooleanFormula result = wrapBool(greaterThan(extractInfo(str1), extractInfo(str2)));
8080
if (Generator.isLoggingEnabled()) {
81-
throw new UnsupportedOperationException("SMTLIB does not allow greater "
82-
+ "than or equal to StringFormula! Use str.< or str.<= instead.");
81+
throw new UnsupportedOperationException(
82+
"SMTLIB does not allow greater "
83+
+ "than or equal to StringFormula! Use str.< or str.<= instead.");
8384
}
8485
return result;
8586
}
@@ -90,8 +91,9 @@ public BooleanFormula greaterThan(StringFormula str1, StringFormula str2) {
9091
public BooleanFormula greaterOrEquals(StringFormula str1, StringFormula str2) {
9192
BooleanFormula result = wrapBool(greaterOrEquals(extractInfo(str1), extractInfo(str2)));
9293
if (Generator.isLoggingEnabled()) {
93-
throw new UnsupportedOperationException("SMTLIB does not allow greater "
94-
+ "than or equal to StringFormula! Use str.< or str.<= instead.");
94+
throw new UnsupportedOperationException(
95+
"SMTLIB does not allow greater "
96+
+ "than or equal to StringFormula! Use str.< or str.<= instead.");
9597
}
9698
return result;
9799
}

‎src/org/sosy_lab/java_smt/basicimpl/StringGenerator.java‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -184,7 +184,10 @@ protected static void logRegexOptional(RegexFormula result, RegexFormula regex)
184184
}
185185

186186
protected static void logRegexTimes(RegexFormula result, RegexFormula regex, int repetitions) {
187-
logOperation(result, ImmutableList.of(regex, repetitions), "((_ re.^ "+repetitions+") %s)",
187+
logOperation(
188+
result,
189+
ImmutableList.of(regex, repetitions),
190+
"((_ re.^ " + repetitions + ") %s)",
188191
Keyword.SKIP);
189192
}
190193

‎src/org/sosy_lab/java_smt/test/FloatingPointSMTLIB2GeneratorTest.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -462,7 +462,8 @@ public void testRound() {
462462
String actualResult = String.valueOf(Generator.getLines());
463463

464464
String expectedResult =
465-
"(declare-const a (_ FloatingPoint 8 24))\n" + "(assert (fp.eq a (fp.roundToIntegral RNE "
465+
"(declare-const a (_ FloatingPoint 8 24))\n"
466+
+ "(assert (fp.eq a (fp.roundToIntegral RNE "
466467
+ "a)))\n";
467468

468469
assertThat(actualResult).isEqualTo(expectedResult);

‎src/org/sosy_lab/java_smt/test/StringSMTLIB2GeneratorTest.java‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,16 +7,13 @@
77

88
import static com.google.common.truth.Truth.assertThat;
99

10-
import java.io.IOException;
1110
import java.util.List;
1211
import java.util.Objects;
1312
import org.junit.Test;
1413
import org.sosy_lab.common.configuration.ConfigurationBuilder;
15-
import org.sosy_lab.common.configuration.InvalidConfigurationException;
1614
import org.sosy_lab.java_smt.api.BooleanFormula;
1715
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
1816
import org.sosy_lab.java_smt.api.RegexFormula;
19-
import org.sosy_lab.java_smt.api.SolverException;
2017
import org.sosy_lab.java_smt.api.StringFormula;
2118
import org.sosy_lab.java_smt.basicimpl.Generator;
2219

‎src/org/sosy_lab/java_smt/utils/ParseGenerateAndReparse.java‎

Lines changed: 23 additions & 139 deletions
Original file line numberDiff line numberDiff line change
@@ -4,16 +4,12 @@
44
// SPDX-License-Identifier: Apache-2.0
55
package org.sosy_lab.java_smt.utils;
66

7+
import com.microsoft.z3.*;
78
import com.microsoft.z3.Context;
8-
import com.microsoft.z3.Solver;
9-
import edu.stanford.CVC4.ExprManager;
10-
import edu.stanford.CVC4.SExpr;
11-
import edu.stanford.CVC4.SmtEngine;
129
import java.io.IOException;
1310
import java.nio.charset.Charset;
1411
import java.nio.file.Files;
1512
import java.nio.file.Path;
16-
import java.nio.file.Paths;
1713
import java.util.Locale;
1814
import org.sosy_lab.common.ShutdownManager;
1915
import org.sosy_lab.common.configuration.Configuration;
@@ -28,29 +24,24 @@
2824
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
2925
import org.sosy_lab.java_smt.api.SolverException;
3026
import org.sosy_lab.java_smt.basicimpl.Generator;
31-
import com.microsoft.z3.*;
32-
import io.github.cvc5.*;
33-
import java.io.*;
34-
import java.nio.file.*;
35-
import io.github.cvc5.*;
36-
import io.github.cvc5.modes.*;
3727

38-
/**
39-
* This file is meant for the Evaluation of the Parser/Generator.
40-
*/
28+
/** This file is meant for the Evaluation of the Parser/Generator. */
4129
class ParseGenerateAndReparse {
42-
private ParseGenerateAndReparse() {
43-
}
30+
private ParseGenerateAndReparse() {}
4431

4532
public static void main(String[] args)
4633
throws InvalidConfigurationException, InterruptedException, SolverException {
47-
34+
String expectedResult =
35+
"(declare-const a (_ FloatingPoint 8 24))\n"
36+
+ "(declare-const b (_ FloatingPoint 8 24))\n"
37+
+ "(declare-const min (_ FloatingPoint 8 24))\n"
38+
+ "(assert (fp.eq (fp.min a b) min))\n";
39+
System.out.println(nativeZ3ParseAndIsUnsat(expectedResult));
4840
if (args.length < 3) {
4941
System.err.println("Usage: java ParseGenerateAndReparseTest <smt2-file> <solver> <mode>");
5042
System.exit(1);
5143
}
5244

53-
5445
String smt2FilePath = args[0];
5546
String smt2;
5647
try {
@@ -83,8 +74,8 @@ public static void main(String[] args)
8374
if (mode.equals("GENERATE_AND_REPARSE")) {
8475
// PARSE REGENERATE THEN NATIVE PARSE
8576
try (SolverContext solverLessContext =
86-
SolverContextFactory.createSolverContext(
87-
config, logger, shutdown.getNotifier(), Solvers.SOLVERLESS)) {
77+
SolverContextFactory.createSolverContext(
78+
config, logger, shutdown.getNotifier(), Solvers.SOLVERLESS)) {
8879

8980
// JAVASMT'S PARSER
9081
BooleanFormula formula =
@@ -93,39 +84,31 @@ public static void main(String[] args)
9384
Generator.assembleConstraint(formula);
9485
String regenerated = Generator.getSMTLIB2String();
9586
// NATIVE PARSE
96-
checkResult(callNativeParseAndIsUnsat(solver, smt2FilePath));
87+
checkResult(nativeZ3ParseAndIsUnsat(regenerated));
9788
} catch (Exception pE) {
9889
printError(pE);
9990
}
100-
10191
}
10292
if (mode.equals("NATIVE")) {
103-
try (SolverContext realSolverContext =
104-
SolverContextFactory.createSolverContext(
105-
config, logger, shutdown.getNotifier(), solver);
106-
ProverEnvironment realProverEnvironment =
107-
realSolverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
108-
109-
try {
110-
// NATIVE PARSE
111-
checkResult(callNativeParseAndIsUnsat(solver, smt2FilePath));
112-
} catch (Exception pE) {
113-
printError(pE);
114-
}
93+
try {
94+
// NATIVE PARSE
95+
checkResult(nativeZ3ParseAndIsUnsat(smt2FilePath));
96+
} catch (Exception pE) {
97+
printError(pE);
11598
}
11699
}
117100
if (mode.equals("PARSE")) {
118101
try (SolverContext realSolverContext =
119-
SolverContextFactory.createSolverContext(
120-
config, logger, shutdown.getNotifier(), solver);
121-
ProverEnvironment realProverEnvironment =
122-
realSolverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
102+
SolverContextFactory.createSolverContext(
103+
config, logger, shutdown.getNotifier(), solver);
104+
ProverEnvironment realProverEnvironment =
105+
realSolverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
123106
try {
124107
// JAVASMT'S PARSER
125108
BooleanFormula javaSMTParsed =
126109
realSolverContext.getFormulaManager().universalParseFromString(smt2);
127110
realProverEnvironment.addConstraint(javaSMTParsed);
128-
//JAVASMT'S PARSE
111+
// JAVASMT'S PARSE
129112
checkResult(realProverEnvironment.isUnsat());
130113
} catch (Exception pE) {
131114
printError(pE);
@@ -139,7 +122,7 @@ public static void checkResult(boolean isUnsat) {
139122
System.exit(0);
140123
}
141124

142-
public static boolean nativeZ3ParseAndIsUnsat(String smt2) throws Exception {
125+
public static boolean nativeZ3ParseAndIsUnsat(String smt2) {
143126
try (Context ctx = new Context()) {
144127
Solver solver = ctx.mkSolver();
145128
solver.fromString(smt2);
@@ -148,105 +131,6 @@ public static boolean nativeZ3ParseAndIsUnsat(String smt2) throws Exception {
148131
}
149132
}
150133

151-
public static boolean nativeCVC5ParseAndIsUnsat(String smt2) throws Exception {
152-
// 1. Temporäre Datei erstellen
153-
Path tempFile = Files.createTempFile("cvc5_", ".smt2");
154-
try {
155-
// 2. SMT2-Inhalt in temporäre Datei schreiben
156-
Files.write(tempFile, smt2.getBytes());
157-
158-
// 3. Prozess für CVC5 starten
159-
ProcessBuilder pb = new ProcessBuilder(
160-
"./dependencies/cvc5",
161-
"--lang=smt2",
162-
tempFile.toString()
163-
);
164-
pb.redirectErrorStream(true);
165-
Process process = pb.start();
166-
167-
// 4. Ausgabe lesen
168-
try (BufferedReader reader = new BufferedReader(
169-
new InputStreamReader(process.getInputStream()))) {
170-
String line;
171-
while ((line = reader.readLine()) != null) {
172-
if (line.trim().equals("unsat")) {
173-
return true;
174-
} else if (line.trim().equals("sat")) {
175-
return false;
176-
}
177-
}
178-
}
179-
180-
// 5. Auf Prozessende warten
181-
int exitCode = process.waitFor();
182-
if (exitCode != 0) {
183-
throw new RuntimeException("CVC5 exited with code " + exitCode);
184-
}
185-
186-
return false; // unknown
187-
} finally {
188-
// 6. Temporäre Datei löschen
189-
Files.deleteIfExists(tempFile);
190-
}
191-
}
192-
193-
public static boolean nativeCVC4ParseAndIsUnsat(String smt2) throws Exception {
194-
// 1. Temporäre Datei erstellen
195-
Path tempFile = Files.createTempFile("cvc4_", ".smt2");
196-
try {
197-
// 2. SMT2-Inhalt in temporäre Datei schreiben
198-
Files.write(tempFile, smt2.getBytes());
199-
200-
// 3. Prozess für CVC4 starten
201-
ProcessBuilder pb = new ProcessBuilder(
202-
"./dependencies/cvc4",
203-
"--lang=smt2",
204-
tempFile.toString()
205-
);
206-
pb.redirectErrorStream(true);
207-
Process process = pb.start();
208-
209-
// 4. Ausgabe lesen
210-
try (BufferedReader reader = new BufferedReader(
211-
new InputStreamReader(process.getInputStream()))) {
212-
String line;
213-
while ((line = reader.readLine()) != null) {
214-
if (line.trim().equals("unsat")) {
215-
return true;
216-
} else if (line.trim().equals("sat")) {
217-
return false;
218-
}
219-
}
220-
}
221-
222-
// 5. Auf Prozessende warten
223-
int exitCode = process.waitFor();
224-
if (exitCode != 0) {
225-
throw new RuntimeException("CVC4 exited with code " + exitCode);
226-
}
227-
228-
return false; // unknown
229-
} finally {
230-
// 6. Temporäre Datei löschen
231-
Files.deleteIfExists(tempFile);
232-
}
233-
}
234-
235-
public static boolean callNativeParseAndIsUnsat(Solvers solverName, String smt2)
236-
throws Exception {
237-
switch (solverName) {
238-
case Z3:
239-
return nativeZ3ParseAndIsUnsat(smt2);
240-
case CVC4:
241-
return nativeCVC4ParseAndIsUnsat(smt2);
242-
case CVC5:
243-
return nativeCVC5ParseAndIsUnsat(smt2);
244-
default:
245-
throw new UnsupportedOperationException("Unsupported solver: " + solverName);
246-
}
247-
}
248-
249-
250134
public static void printError(Exception pE) {
251135
System.out.println("ERROR: ");
252136
pE.printStackTrace();

0 commit comments

Comments
 (0)