Skip to content

Commit

Permalink
apply fixes for updated dependencies: formatting and locale-settings.
Browse files Browse the repository at this point in the history
  • Loading branch information
kfriedberger committed Jun 1, 2023
1 parent f909412 commit 8e9ad5c
Show file tree
Hide file tree
Showing 13 changed files with 45 additions and 44 deletions.
2 changes: 1 addition & 1 deletion .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ variables:
# Version of https://gitlab.com/sosy-lab/software/refaster/ to use
REFASTER_REPO_REVISION: 31cd8ffc4966957e156665dbba76679ade5bb5c9
# Needs to be synchronized with Error Prone version in lib/ivy.xml
REFASTER_VERSION: 2.18.0
REFASTER_VERSION: 2.19.1

build:jdk-17:
variables:
Expand Down
1 change: 1 addition & 0 deletions src/org/sosy_lab/java_smt/example/NQueens.java
Original file line number Diff line number Diff line change
Expand Up @@ -181,6 +181,7 @@ private List<BooleanFormula> columnRule(BooleanFormula[][] symbols) {
}
return rules;
}

/**
* Rule 4: At most one queen per diagonal transform the field (=symbols) from square shape into a
* (downwards/upwards directed) rhombus that is embedded in a rectangle
Expand Down
3 changes: 2 additions & 1 deletion src/org/sosy_lab/java_smt/example/PrettyPrinter.java
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
import java.nio.file.Path;
import java.util.ArrayList;
import java.util.List;
import java.util.Locale;
import java.util.logging.Level;
import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.common.configuration.Configuration;
Expand Down Expand Up @@ -63,7 +64,7 @@ public static void main(String... args)
if (arg.startsWith("-solver=")) {
solver = Solvers.valueOf(arg.substring(8));
} else if (arg.startsWith("-type=")) {
type = Type.valueOf(arg.substring(6).toUpperCase());
type = Type.valueOf(arg.substring(6).toUpperCase(Locale.getDefault()));
} else if (path == null) {
path = Path.of(arg);
} else {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ public class BoolectorFormulaCreator extends FormulaCreator<Long, Long, Long, Lo

// Remember uf sorts, as Boolector does not give them back correctly
private final Map<Long, List<Long>> ufArgumentsSortMap = new HashMap<>();

// Possibly we need to split this up into vars, ufs, and arrays

BoolectorFormulaCreator(Long btor) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
import com.google.common.collect.ImmutableList;
import com.google.common.collect.ImmutableMap;
import java.util.Arrays;
import java.util.Locale;
import org.junit.After;
import org.junit.AssumptionViolatedException;
import org.junit.Before;
Expand Down Expand Up @@ -75,7 +76,9 @@ public void optionNameTest() {
// check whether our enum is identical to Boolector's internal enum
for (BtorOption option : BtorOption.values()) {
String optName = BtorJNI.boolector_get_opt_lng(btor, option.getValue());
String converted = "BTOR_OPT_" + optName.replace("-", "_").replace(":", "_").toUpperCase();
String converted =
"BTOR_OPT_"
+ optName.replace("-", "_").replace(":", "_").toUpperCase(Locale.getDefault());
assertThat(option.name()).isEqualTo(ALLOWED_DIFFS.getOrDefault(converted, converted));
}
}
Expand All @@ -85,7 +88,7 @@ public void satSolverTest() {
// check whether all sat solvers are available
for (SatSolver satSolver : SatSolver.values()) {
long btor1 = BtorJNI.boolector_new();
BtorJNI.boolector_set_sat_solver(btor1, satSolver.name().toLowerCase());
BtorJNI.boolector_set_sat_solver(btor1, satSolver.name().toLowerCase(Locale.getDefault()));
long newVar = BtorJNI.boolector_var(btor1, BtorJNI.boolector_bool_sort(btor1), "x");
BtorJNI.boolector_assert(btor1, newVar);
int result = BtorJNI.boolector_sat(btor1);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
import com.google.common.base.Splitter;
import com.google.common.base.Splitter.MapSplitter;
import com.google.common.collect.ImmutableMap;
import java.util.Locale;
import java.util.Map;
import java.util.Set;
import java.util.concurrent.atomic.AtomicBoolean;
Expand Down Expand Up @@ -227,7 +228,8 @@ private static void setOptions(
BoolectorSettings settings = new BoolectorSettings(config);

Preconditions.checkNotNull(settings.satSolver);
BtorJNI.boolector_set_sat_solver(btor, settings.satSolver.name().toLowerCase());
BtorJNI.boolector_set_sat_solver(
btor, settings.satSolver.name().toLowerCase(Locale.getDefault()));
// Default Options to enable multiple SAT, auto cleanup on close, incremental mode
BtorJNI.boolector_set_opt(btor, BtorOption.BTOR_OPT_MODEL_GEN.getValue(), 2);
// Auto memory clean after closing
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -696,6 +696,7 @@ public static native long msat_simplify(
public static native String msat_decl_get_name(long d);

public static native String msat_term_repr(long t);

/*
* Parsing and writing formulas.
*/
Expand Down Expand Up @@ -727,6 +728,7 @@ public static native long msat_simplify(
public static native void msat_reset_env(long e);

public static native void msat_assert_formula(long e, long formula);

// public static native int msat_add_preferred_for_branching(long e, long termBoolvar);
// public static native int msat_clear_preferred_for_branching(long e)
private static native int msat_solve(long e) throws InterruptedException;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ protected Integer not(Integer pParam1) {
protected Integer and(Integer pParam1, Integer pParam2) {
return yices_and2(pParam1, pParam2);
}

// Causes BooleanFormulaManagerTest/testConjunctionCollector to fail.
// @Override
// protected Integer andImpl(Collection<Integer> pParams) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
import com.google.common.base.Preconditions;
import com.google.common.base.Strings;
import java.io.IOException;
import java.util.Locale;
import java.util.Map;
import org.sosy_lab.common.Appender;
import org.sosy_lab.common.Appenders;
Expand Down Expand Up @@ -122,7 +123,7 @@ private String getTypeRepr(int type) {
return "(_ BitVec " + yices_bvtype_size(type) + ")";
}
String typeRepr = yices_type_to_string(type);
return typeRepr.substring(0, 1).toUpperCase() + typeRepr.substring(1);
return typeRepr.substring(0, 1).toUpperCase(Locale.getDefault()) + typeRepr.substring(1);
}
};
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -612,6 +612,7 @@ private Yices2NativeApi() {}
// TODO can return up to UINT32_MAX ?
/** Returns an array in the form [term,power]. */
public static native int[] yices_product_component(int t, int i);

/*
* SAT Checking
*/
Expand Down
56 changes: 21 additions & 35 deletions src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Locale;
import java.util.concurrent.BlockingQueue;
import java.util.concurrent.ConcurrentLinkedQueue;
import java.util.concurrent.CountDownLatch;
Expand Down Expand Up @@ -113,7 +114,7 @@ protected Solvers solverToUse() {
public void checkThatSolverIsAvailable() throws InvalidConfigurationException {
initSolver().close();

if (System.getProperty("os.name").toLowerCase().startsWith("win")) {
if (System.getProperty("os.name").toLowerCase(Locale.getDefault()).startsWith("win")) {
assume()
.withMessage("MathSAT5 is not reentant on Windows")
.that(solver)
Expand Down Expand Up @@ -194,6 +195,25 @@ public void testBvConcurrencyWithConcurrentContext() {
});
}

/** Helperclass to pack a SolverContext together with a Formula. */
private static class ContextAndFormula {
private final SolverContext context;
private final BooleanFormula formula;

private ContextAndFormula(SolverContext context, BooleanFormula formula) {
this.context = context;
this.formula = formula;
}

SolverContext getContext() {
return context;
}

BooleanFormula getFormula() {
return formula;
}
}

/**
* Test translation of formulas used on distinct contexts to a new, unrelated context. Every
* thread creates a context, generates a formula, those are collected and handed back to the main
Expand All @@ -210,24 +230,7 @@ public void testFormulaTranslationWithConcurrentContexts()
.withMessage("Solver does not support translation of formulas")
.that(solver)
.isNoneOf(Solvers.CVC4, Solvers.PRINCESS, Solvers.CVC5);
/** Helperclass to pack a SolverContext together with a Formula */
class ContextAndFormula {
private final SolverContext context;
private final BooleanFormula formula;

protected ContextAndFormula(SolverContext context, BooleanFormula formula) {
this.context = context;
this.formula = formula;
}

public SolverContext getContext() {
return context;
}

public BooleanFormula getFormula() {
return formula;
}
}
ConcurrentLinkedQueue<ContextAndFormula> contextAndFormulaList = new ConcurrentLinkedQueue<>();

assertConcurrency(
Expand Down Expand Up @@ -439,24 +442,7 @@ public void continuousRunningThreadFormulaTransferTranslateTest() {
.withMessage("Solver does not support translation of formulas")
.that(solver)
.isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS);
/** Helperclass to pack a SolverContext together with a Formula */
class ContextAndFormula {
private final SolverContext context;
private final BooleanFormula formula;

protected ContextAndFormula(SolverContext context, BooleanFormula formula) {
this.context = context;
this.formula = formula;
}

public SolverContext getContext() {
return context;
}

public BooleanFormula getFormula() {
return formula;
}
}
// This is fine! We might access this more than once at a time,
// but that gives only access to the bucket, which is threadsafe.
AtomicReferenceArray<BlockingQueue<ContextAndFormula>> bucketQueue =
Expand Down
3 changes: 2 additions & 1 deletion src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@

import com.google.common.base.StandardSystemProperty;
import com.google.common.truth.StandardSubjectBuilder;
import java.util.Locale;
import org.junit.Before;
import org.junit.Test;
import org.junit.runner.RunWith;
Expand All @@ -36,7 +37,7 @@
public class SolverContextFactoryTest {

private static final String OS =
StandardSystemProperty.OS_NAME.value().toLowerCase().replace(" ", "");
StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", "");
private static final boolean IS_WINDOWS = OS.startsWith("windows");
private static final boolean IS_MAC = OS.startsWith("macos");
private static final boolean IS_LINUX = OS.startsWith("linux");
Expand Down
5 changes: 3 additions & 2 deletions src/org/sosy_lab/java_smt/test/SolverVisitorTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Locale;
import java.util.Map;
import java.util.Random;
import java.util.Set;
Expand Down Expand Up @@ -928,15 +929,15 @@ public BooleanFormula visitAtom(
BooleanFormula pAtom, FunctionDeclaration<BooleanFormula> decl) {
if (decl.getKind() == FunctionDeclarationKind.VAR) {
// Uppercase all variables.
return bmgr.makeVariable(decl.getName().toUpperCase());
return bmgr.makeVariable(decl.getName().toUpperCase(Locale.getDefault()));
} else {
return pAtom;
}
}
});
assertThat(
mgr.extractVariables(transformed).keySet().stream()
.allMatch(pS -> pS.equals(pS.toUpperCase())))
.allMatch(pS -> pS.equals(pS.toUpperCase(Locale.getDefault()))))
.isTrue();
}

Expand Down

0 comments on commit 8e9ad5c

Please sign in to comment.