Skip to content

Commit 785ccd1

Browse files
DavidGalllobDavidGalllob
committed
-changed solvers to native for benchmark
1 parent 2ba04eb commit 785ccd1

File tree

3 files changed

+155
-44
lines changed

3 files changed

+155
-44
lines changed

‎src/org/sosy_lab/java_smt/solvers/SolverLess/SolverLessBooleanFormulaManager.java‎

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -96,15 +96,9 @@ protected SMTLIB2Formula ifThenElse(SMTLIB2Formula cond, SMTLIB2Formula f1, SMTL
9696
return new SMTLIB2Formula(new DummyType(DummyType.Type.BOOLEAN));
9797
}
9898
if (Boolean.parseBoolean(cond.getValue())) {
99-
if (Objects.equals(f1.getValue(), "")) {
100-
return new SMTLIB2Formula(new DummyType(DummyType.Type.BOOLEAN));
101-
}
102-
return new SMTLIB2Formula(Boolean.parseBoolean(f1.getValue()));
99+
return f1;
103100
} else {
104-
if (Objects.equals(f2.getValue(), "")) {
105-
return new SMTLIB2Formula(new DummyType(DummyType.Type.BOOLEAN));
106-
}
107-
return new SMTLIB2Formula(Boolean.parseBoolean(f2.getValue()));
101+
return f2;
108102
}
109103
}
110104
}

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

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

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

10+
import java.io.IOException;
1011
import java.util.List;
1112
import java.util.Objects;
1213
import org.junit.Test;
1314
import org.sosy_lab.common.configuration.ConfigurationBuilder;
15+
import org.sosy_lab.common.configuration.InvalidConfigurationException;
1416
import org.sosy_lab.java_smt.api.BooleanFormula;
1517
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
1618
import org.sosy_lab.java_smt.api.RegexFormula;
19+
import org.sosy_lab.java_smt.api.SolverException;
1720
import org.sosy_lab.java_smt.api.StringFormula;
1821
import org.sosy_lab.java_smt.basicimpl.Generator;
1922

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

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

7+
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;
712
import java.io.IOException;
813
import java.nio.charset.Charset;
914
import java.nio.file.Files;
1015
import java.nio.file.Path;
16+
import java.nio.file.Paths;
1117
import java.util.Locale;
1218
import org.sosy_lab.common.ShutdownManager;
1319
import org.sosy_lab.common.configuration.Configuration;
@@ -22,10 +28,19 @@
2228
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
2329
import org.sosy_lab.java_smt.api.SolverException;
2430
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.*;
2537

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

3045
public static void main(String[] args)
3146
throws InvalidConfigurationException, InterruptedException, SolverException {
@@ -35,6 +50,7 @@ public static void main(String[] args)
3550
System.exit(1);
3651
}
3752

53+
3854
String smt2FilePath = args[0];
3955
String smt2;
4056
try {
@@ -66,60 +82,50 @@ public static void main(String[] args)
6682

6783
if (mode.equals("GENERATE_AND_REPARSE")) {
6884
// PARSE REGENERATE THEN NATIVE PARSE
69-
try (SolverContext realSolverContext =
70-
SolverContextFactory.createSolverContext(
71-
config, logger, shutdown.getNotifier(), solver);
72-
SolverContext solverLessContext =
73-
SolverContextFactory.createSolverContext(
74-
config, logger, shutdown.getNotifier(), Solvers.SOLVERLESS);
75-
ProverEnvironment realProverEnvironment =
76-
realSolverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
85+
try (SolverContext solverLessContext =
86+
SolverContextFactory.createSolverContext(
87+
config, logger, shutdown.getNotifier(), Solvers.SOLVERLESS)) {
7788

78-
try {
79-
// JAVASMT'S PARSER
80-
BooleanFormula formula =
81-
solverLessContext.getFormulaManager().universalParseFromString(smt2);
82-
// JAVASMT'S GENERATOR
83-
Generator.assembleConstraint(formula);
84-
String regenerated = Generator.getSMTLIB2String();
85-
// NATIVE PARSE
86-
BooleanFormula reparsed = realSolverContext.getFormulaManager().parse(regenerated);
87-
realProverEnvironment.addConstraint(reparsed);
88-
checkResult(realProverEnvironment.isUnsat());
89-
90-
} catch (Exception pE) {
91-
printError(pE);
92-
}
89+
// JAVASMT'S PARSER
90+
BooleanFormula formula =
91+
solverLessContext.getFormulaManager().universalParseFromString(smt2);
92+
// JAVASMT'S GENERATOR
93+
Generator.assembleConstraint(formula);
94+
String regenerated = Generator.getSMTLIB2String();
95+
// NATIVE PARSE
96+
checkResult(callNativeParseAndIsUnsat(solver, smt2FilePath));
97+
} catch (Exception pE) {
98+
printError(pE);
9399
}
100+
94101
}
95102
if (mode.equals("NATIVE")) {
96103
try (SolverContext realSolverContext =
97-
SolverContextFactory.createSolverContext(
98-
config, logger, shutdown.getNotifier(), solver);
99-
ProverEnvironment realProverEnvironment =
100-
realSolverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
104+
SolverContextFactory.createSolverContext(
105+
config, logger, shutdown.getNotifier(), solver);
106+
ProverEnvironment realProverEnvironment =
107+
realSolverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
101108

102109
try {
103110
// NATIVE PARSE
104-
BooleanFormula nativeParsed = realSolverContext.getFormulaManager().parse(smt2);
105-
realProverEnvironment.addConstraint(nativeParsed);
106-
checkResult(realProverEnvironment.isUnsat());
111+
checkResult(callNativeParseAndIsUnsat(solver, smt2FilePath));
107112
} catch (Exception pE) {
108113
printError(pE);
109114
}
110115
}
111116
}
112117
if (mode.equals("PARSE")) {
113118
try (SolverContext realSolverContext =
114-
SolverContextFactory.createSolverContext(
115-
config, logger, shutdown.getNotifier(), solver);
116-
ProverEnvironment realProverEnvironment =
117-
realSolverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
119+
SolverContextFactory.createSolverContext(
120+
config, logger, shutdown.getNotifier(), solver);
121+
ProverEnvironment realProverEnvironment =
122+
realSolverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
118123
try {
119124
// JAVASMT'S PARSER
120125
BooleanFormula javaSMTParsed =
121126
realSolverContext.getFormulaManager().universalParseFromString(smt2);
122127
realProverEnvironment.addConstraint(javaSMTParsed);
128+
//JAVASMT'S PARSE
123129
checkResult(realProverEnvironment.isUnsat());
124130
} catch (Exception pE) {
125131
printError(pE);
@@ -133,6 +139,114 @@ public static void checkResult(boolean isUnsat) {
133139
System.exit(0);
134140
}
135141

142+
public static boolean nativeZ3ParseAndIsUnsat(String smt2) throws Exception {
143+
try (Context ctx = new Context()) {
144+
Solver solver = ctx.mkSolver();
145+
solver.fromString(smt2);
146+
Status status = solver.check();
147+
return status == Status.UNSATISFIABLE;
148+
}
149+
}
150+
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+
136250
public static void printError(Exception pE) {
137251
System.out.println("ERROR: ");
138252
pE.printStackTrace();

0 commit comments

Comments
 (0)