Skip to content

Commit a909475

Browse files
committed
-refactorings
1 parent ed2208f commit a909475

File tree

3 files changed

+23
-8
lines changed

3 files changed

+23
-8
lines changed

.gitignore

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,3 +63,11 @@ retrieve-jars.sh
6363
/.apt-generated/
6464
/repository
6565
pom.xml
66+
/Checkstyle.html
67+
/Checkstyle.Test.html
68+
/Checkstyle.Test.xml
69+
/Checkstyle.xml
70+
/JUnit.html
71+
/local_test_run
72+
/rule.refaster
73+
/SpotBugs.xml

src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Visitor.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -968,7 +968,8 @@ public Object visitMultiterm(MultitermContext ctx) {
968968
return Objects.requireNonNull(imgr).distinct(integerOperands);
969969
}
970970
} catch (Exception e) {
971-
throw new UnsupportedOperationException("JavaSMT support distinct only for numeral types!");
971+
throw new UnsupportedOperationException(
972+
"JavaSMT support distinct only for numeral types!");
972973
}
973974
} else {
974975
throw new ParserException(operator + " takes at least one numeral operand as input. ");

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

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -115,13 +115,18 @@ public static void checkResult(boolean isUnsat) {
115115
System.out.println("SUCCESS: isUnsat = " + isUnsat);
116116
System.exit(0);
117117
}
118+
118119
public static boolean checkNativeParseAndIsUnsat(Solvers solver, String smt2)
119120
throws SolverException, InterruptedException, InvalidConfigurationException {
120-
switch (solver){
121-
case Z3: return nativeZ3ParseAndIsUnsat(smt2);
122-
case MATHSAT5: return nativeMathSatParseAndIsUnsat(smt2);
123-
case BITWUZLA: return nativeBitwuzlaParseAndIsUnsat(smt2);
124-
default: throw new SolverException("Unsupported solver: " + solver);
121+
switch (solver) {
122+
case Z3:
123+
return nativeZ3ParseAndIsUnsat(smt2);
124+
case MATHSAT5:
125+
return nativeMathSatParseAndIsUnsat(smt2);
126+
case BITWUZLA:
127+
return nativeBitwuzlaParseAndIsUnsat(smt2);
128+
default:
129+
throw new SolverException("Unsupported solver: " + solver);
125130
}
126131
}
127132

@@ -133,6 +138,7 @@ public static boolean nativeZ3ParseAndIsUnsat(String smt2) {
133138
return status == Status.UNSATISFIABLE;
134139
}
135140
}
141+
136142
public static boolean nativeBitwuzlaParseAndIsUnsat(String smt2)
137143
throws InvalidConfigurationException, InterruptedException, SolverException {
138144
SolverContext bitwuz = SolverContextFactory.createSolverContext(Solvers.BITWUZLA);
@@ -150,9 +156,9 @@ public static boolean nativeMathSatParseAndIsUnsat(String smt2)
150156
}
151157

152158
public static void printError(Exception pE) {
153-
if(pE instanceof UnsupportedOperationException){
159+
if (pE instanceof UnsupportedOperationException) {
154160
System.out.println("UNSUPPORTED: ");
155-
}else{
161+
} else {
156162
System.out.println("ERROR: ");
157163
}
158164
pE.printStackTrace();

0 commit comments

Comments
 (0)