Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

339 stackoverflowerror using mathsat5 #345

Merged
merged 46 commits into from
Jan 3, 2024
Merged
Show file tree
Hide file tree
Changes from 45 commits
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
02d93be
Added tests to narrow down bug #339. So far no luck, but we did stumb…
daniel-raffler Dec 8, 2023
65e4c32
Fix build issues.
daniel-raffler Dec 10, 2023
5e1f046
Fixed checkstyle errors.
daniel-raffler Dec 10, 2023
fb3d922
Fixed license header.
daniel-raffler Dec 10, 2023
f02f9ad
Fixed nonlocalContext test in SolverThreadLocalTest.
daniel-raffler Dec 10, 2023
202722b
Fixed bug in nonlocalContext test.
daniel-raffler Dec 10, 2023
01c3ce4
Make sure new context gets closed in SolverThreadLocal.nonlocalContext.
daniel-raffler Dec 10, 2023
4003c34
Added assertion to check if ShutdownNotifer was actually triggered wh…
daniel-raffler Dec 14, 2023
6e356cb
Suppress resource warnings when using Executors.newSingleThreadExecutor.
daniel-raffler Dec 14, 2023
c8c7712
Rewrote termination check for MathSAT to address the failed assertion…
daniel-raffler Dec 14, 2023
3196f7f
Fixed formating
daniel-raffler Dec 14, 2023
9e2abee
Added tests for interpolation to SolverThreadLocalTest. This includes…
daniel-raffler Dec 14, 2023
8871155
Simplified nonLocalProverTest
daniel-raffler Dec 14, 2023
d78b8f4
Added a minimal test case for bug #339.
daniel-raffler Dec 14, 2023
9197ed1
Added a native version of the testcase for #339.
daniel-raffler Dec 15, 2023
74f4a25
Fixed formating
daniel-raffler Dec 15, 2023
bd81f54
Added another version of the native test for #339 that fixes the bug.
daniel-raffler Dec 15, 2023
4464c90
Bugfix for #339
daniel-raffler Dec 15, 2023
7adc7be
Revert "Rewrote termination check for MathSAT to address the failed a…
daniel-raffler Dec 15, 2023
9162b20
Revert "Added assertion to check if ShutdownNotifer was actually trig…
daniel-raffler Dec 15, 2023
c41df5c
Disabled failing tests for CVC5
daniel-raffler Dec 15, 2023
e7fda3d
Added copyright header to Bug339Test.java
daniel-raffler Dec 15, 2023
63f8a94
Fixed annotation for bug330BrokenTest: we expect this to fail
daniel-raffler Dec 15, 2023
ea5b9e7
Applied refaster patch
daniel-raffler Dec 15, 2023
0436959
Progage InterruptedExceptionin Mathsat5AbstractProver.exec() to fix s…
daniel-raffler Dec 15, 2023
dc5ee89
Cleaned up SolverThreadLocalTest class
daniel-raffler Dec 19, 2023
1e0319b
Renamed SolverThreadLocalTest class to SolverThreadLocalityTest
daniel-raffler Dec 19, 2023
0b3c2b8
Some clean-up
daniel-raffler Dec 19, 2023
80ede24
Added one more test to SolverThreadLocalityTest that checks what happ…
daniel-raffler Dec 19, 2023
36919ed
Removed native API test for bug339 as it has been fixed.
daniel-raffler Dec 19, 2023
d1e85eb
Removed JavaSMT test class for bug339 as it has been fixed.
daniel-raffler Dec 19, 2023
389af9f
Removed unused imports.
daniel-raffler Dec 19, 2023
010ddc2
Remove use of "synchornized" in Mathsat5AbstractProver. Mathsat only …
daniel-raffler Dec 19, 2023
a28e7cd
Remove use of "synchornized" in Mathsat5InterpolatingProver.
daniel-raffler Dec 19, 2023
24d16e6
Remove comment about bug #339 from SolverThreadLocalityTest as the is…
daniel-raffler Dec 19, 2023
7b70824
Fixed resource leak in SolverThreadLocalityTest. See https://github.c…
daniel-raffler Dec 20, 2023
7bde6ff
Fixed a bug in SolverThreadLocalityTest.nonlocalInterpolationTest whe…
daniel-raffler Dec 20, 2023
0fa64d4
SolverThreadLocalityTest: Moved hard problem generator global for all…
daniel-raffler Dec 20, 2023
4246d86
SolverThreadLocalityTest: Don't catch InvalidConfigurationExceptions …
daniel-raffler Dec 20, 2023
57ca2f4
MathSAT5AbstractProver: Remove the helper method exec and install the…
daniel-raffler Dec 20, 2023
c18121a
Fixed checkstyle warning
daniel-raffler Dec 20, 2023
0f14370
Try and fix the AppVeyor issue.
daniel-raffler Dec 20, 2023
151c2ed
Removed unnecessary "resource" annotations.
daniel-raffler Dec 20, 2023
9b1361c
MathSAT: shorten some code and refactor callback-providing method.
kfriedberger Dec 26, 2023
85c6def
Test: improve and extend some documentation.
kfriedberger Dec 26, 2023
3ce7326
Fixed nonLocalProverTest: To trigger this specific bug in CVC5 we nee…
daniel-raffler Dec 29, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_pop_backtrack_point;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_push_backtrack_point;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_arg;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_boolean_constant;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_not;
Expand Down Expand Up @@ -57,7 +58,6 @@ abstract class Mathsat5AbstractProver<T2> extends AbstractProver<T2> {
protected final Mathsat5SolverContext context;
protected final long curEnv;
private final long curConfig;
private final long terminationTest;
protected final Mathsat5FormulaCreator creator;
private final ShutdownNotifier shutdownNotifier;

Expand All @@ -71,7 +71,6 @@ protected Mathsat5AbstractProver(
creator = pCreator;
curConfig = buildConfig(pOptions);
curEnv = context.createEnvironment(curConfig);
terminationTest = context.addTerminationTest(curEnv);
shutdownNotifier = pShutdownNotifier;
}

Expand Down Expand Up @@ -100,15 +99,27 @@ private long buildConfig(Set<ProverOptions> opts) {
@Override
public boolean isUnsat() throws InterruptedException, SolverException {
Preconditions.checkState(!closed);
return !msat_check_sat(curEnv);

final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest());
try {
return !msat_check_sat(curEnv);
} finally {
msat_free_termination_callback(hook);
}
}

@Override
public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
throws SolverException, InterruptedException {
Preconditions.checkState(!closed);
checkForLiterals(pAssumptions);
return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions));

final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest());
try {
return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions));
} finally {
msat_free_termination_callback(hook);
}
}

private void checkForLiterals(Collection<BooleanFormula> formulas) {
Expand Down Expand Up @@ -214,7 +225,6 @@ public ImmutableMap<String, String> getStatistics() {
public void close() {
if (!closed) {
msat_destroy_env(curEnv);
msat_free_termination_callback(terminationTest);
msat_destroy_config(curConfig);
}
super.close();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_env;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_version;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback;

import com.google.common.annotations.VisibleForTesting;
import com.google.common.base.Preconditions;
Expand Down Expand Up @@ -300,9 +299,13 @@ public void close() {
}
}

long addTerminationTest(long env) {
/**
* Get a termination callback for the current context. The callback can be registered upfront,
* i.e., before calling a possibly expensive computation in the solver to allow a proper shutdown.
*/
TerminationCallback getTerminationTest() {
Preconditions.checkState(!closed, "solver context is already closed");
return msat_set_termination_callback(env, terminationTest);
return terminationTest;
}

@Override
Expand Down
Loading