Skip to content

Commit 0f8e757

Browse files
author
BaierD
committed
Add default handling for basic prover API like isUnsat(), getUnsatCore() etc. so that interrupts and common prerequisites are uniformly handled
1 parent 5de5971 commit 0f8e757

19 files changed

+167
-182
lines changed

‎src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,13 @@
2424
* provides only the common operations. In most cases, just use one of the two sub-interfaces
2525
*/
2626
public interface BasicProverEnvironment<T> extends AutoCloseable {
27+
String NO_MODEL_HELP = "Model computation failed. Are the pushed formulae " + "satisfiable?";
2728

28-
String NO_MODEL_HELP = "Model computation failed. Are the pushed formulae satisfiable?";
29+
String NO_UNSAT_CORE_HELP =
30+
"UnsatCore computation failed. Are the pushed formulae " + "unsatisfiable?";
31+
32+
String STACK_CHANGED_HELP =
33+
"Computation failed. The prover state has changed since the last " + "call to isUnsat().";
2934

3035
/**
3136
* Push a backtracking point and add a formula to the current stack, asserting it. The return
@@ -109,11 +114,7 @@ default Evaluator getEvaluator() throws SolverException {
109114
* <p>Note that if you need to iterate multiple times over the model it may be more efficient to
110115
* use this method instead of {@link #getModel()} (depending on the solver).
111116
*/
112-
default ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
113-
try (Model model = getModel()) {
114-
return model.asList();
115-
}
116-
}
117+
ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException;
117118

118119
/**
119120
* Get an unsat core. This should be called only immediately after an {@link #isUnsat()} call that

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

Lines changed: 75 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,15 +18,18 @@
1818
import com.google.common.collect.Multimap;
1919
import com.google.errorprone.annotations.CanIgnoreReturnValue;
2020
import java.util.ArrayList;
21+
import java.util.Collection;
2122
import java.util.LinkedHashSet;
2223
import java.util.List;
24+
import java.util.Optional;
2325
import java.util.Set;
2426
import org.checkerframework.checker.nullness.qual.Nullable;
2527
import org.sosy_lab.common.ShutdownManager;
2628
import org.sosy_lab.common.ShutdownNotifier;
2729
import org.sosy_lab.java_smt.api.BasicProverEnvironment;
2830
import org.sosy_lab.java_smt.api.BooleanFormula;
2931
import org.sosy_lab.java_smt.api.Evaluator;
32+
import org.sosy_lab.java_smt.api.Model;
3033
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
3134
import org.sosy_lab.java_smt.api.SolverException;
3235

@@ -38,6 +41,8 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
3841
private final boolean generateUnsatCoresOverAssumptions;
3942
protected final boolean enableSL;
4043
protected boolean closed = false;
44+
protected boolean wasLastSatCheckSat = false;
45+
protected boolean stackChangedSinceLastQuery = false;
4146

4247
private final Set<Evaluator> evaluators = new LinkedHashSet<>();
4348

@@ -75,11 +80,11 @@ protected final void checkGenerateAllSat() {
7580
Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT);
7681
}
7782

78-
protected final void checkGenerateUnsatCores() {
83+
private final void checkGenerateUnsatCores() {
7984
Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE);
8085
}
8186

82-
protected final void checkGenerateUnsatCoresOverAssumptions() {
87+
private final void checkGenerateUnsatCoresOverAssumptions() {
8388
Preconditions.checkState(
8489
generateUnsatCoresOverAssumptions,
8590
TEMPLATE,
@@ -99,18 +104,68 @@ public int size() {
99104
@Override
100105
public final boolean isUnsat() throws SolverException, InterruptedException {
101106
checkState(!closed);
102-
closeAllEvaluators(); // TODO: needed?
107+
closeAllEvaluators();
103108
proverShutdownNotifier.shutdownIfNecessary();
104-
return isUnsatImpl();
109+
wasLastSatCheckSat = !isUnsatImpl();
110+
stackChangedSinceLastQuery = false;
111+
return !wasLastSatCheckSat;
105112
}
106113

107114
protected abstract boolean isUnsatImpl() throws SolverException, InterruptedException;
108115

116+
@Override
117+
public List<BooleanFormula> getUnsatCore() {
118+
checkState(!closed);
119+
checkState(!proverShutdownNotifier.shouldShutdown());
120+
checkState(!wasLastSatCheckSat, NO_UNSAT_CORE_HELP);
121+
checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP);
122+
checkGenerateUnsatCores();
123+
return getUnsatCoreImpl();
124+
}
125+
126+
protected abstract List<BooleanFormula> getUnsatCoreImpl();
127+
128+
@Override
129+
public final Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
130+
Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
131+
checkState(!closed);
132+
proverShutdownNotifier.shutdownIfNecessary();
133+
checkGenerateUnsatCoresOverAssumptions();
134+
return unsatCoreOverAssumptionsImpl(assumptions);
135+
}
136+
137+
protected abstract Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
138+
Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException;
139+
140+
@Override
141+
public final boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
142+
throws SolverException, InterruptedException {
143+
checkState(!closed);
144+
proverShutdownNotifier.shutdownIfNecessary();
145+
return isUnsatWithAssumptionsImpl(assumptions);
146+
}
147+
148+
protected abstract boolean isUnsatWithAssumptionsImpl(Collection<BooleanFormula> assumptions)
149+
throws SolverException, InterruptedException;
150+
151+
@Override
152+
public final Model getModel() throws SolverException {
153+
checkState(!closed);
154+
checkState(!proverShutdownNotifier.shouldShutdown());
155+
checkState(wasLastSatCheckSat, NO_MODEL_HELP);
156+
checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP);
157+
checkGenerateModels();
158+
return getModelImpl();
159+
}
160+
161+
protected abstract Model getModelImpl() throws SolverException;
162+
109163
@Override
110164
public final void push() throws InterruptedException {
111165
checkState(!closed);
112166
proverShutdownNotifier.shutdownIfNecessary();
113167
pushImpl();
168+
stackChangedSinceLastQuery = true;
114169
assertedFormulas.add(LinkedHashMultimap.create());
115170
}
116171

@@ -121,6 +176,9 @@ public final void pop() {
121176
checkState(!closed);
122177
checkState(assertedFormulas.size() > 1, "initial level must remain until close");
123178
assertedFormulas.remove(assertedFormulas.size() - 1); // remove last
179+
// TODO: technically only needed if the level removed was non empty.
180+
stackChangedSinceLastQuery = true;
181+
wasLastSatCheckSat = false;
124182
popImpl();
125183
}
126184

@@ -133,6 +191,8 @@ public final void pop() {
133191
proverShutdownNotifier.shutdownIfNecessary();
134192
T t = addConstraintImpl(constraint);
135193
Iterables.getLast(assertedFormulas).put(constraint, t);
194+
stackChangedSinceLastQuery = true;
195+
wasLastSatCheckSat = false;
136196
return t;
137197
}
138198

@@ -173,6 +233,17 @@ protected void closeAllEvaluators() {
173233
evaluators.clear();
174234
}
175235

236+
@Override
237+
public ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
238+
Preconditions.checkState(!closed);
239+
checkState(!proverShutdownNotifier.shouldShutdown());
240+
Preconditions.checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP);
241+
checkState(wasLastSatCheckSat);
242+
try (Model model = getModel()) {
243+
return model.asList();
244+
}
245+
}
246+
176247
@Override
177248
public void close() {
178249
assertedFormulas.clear();

‎src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010

1111
import static com.google.common.base.Preconditions.checkNotNull;
1212

13+
import com.google.common.collect.ImmutableList;
1314
import java.util.Collection;
1415
import java.util.List;
1516
import java.util.Optional;
@@ -18,6 +19,7 @@
1819
import org.sosy_lab.java_smt.api.BasicProverEnvironment;
1920
import org.sosy_lab.java_smt.api.BooleanFormula;
2021
import org.sosy_lab.java_smt.api.Model;
22+
import org.sosy_lab.java_smt.api.Model.ValueAssignment;
2123
import org.sosy_lab.java_smt.api.SolverException;
2224

2325
class DebuggingBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
@@ -83,6 +85,11 @@ public Model getModel() throws SolverException {
8385
return new DebuggingModel(delegate.getModel(), debugging);
8486
}
8587

88+
@Override
89+
public ImmutableList<ValueAssignment> getModelAssignments() throws SolverException {
90+
return delegate.getModelAssignments();
91+
}
92+
8693
@Override
8794
public List<BooleanFormula> getUnsatCore() {
8895
debugging.assertThreadLocal();

‎src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010

1111
import static com.google.common.base.Preconditions.checkNotNull;
1212

13+
import com.google.common.collect.ImmutableList;
1314
import java.util.Collection;
1415
import java.util.List;
1516
import java.util.Optional;
@@ -18,6 +19,7 @@
1819
import org.sosy_lab.java_smt.api.BasicProverEnvironment;
1920
import org.sosy_lab.java_smt.api.BooleanFormula;
2021
import org.sosy_lab.java_smt.api.Model;
22+
import org.sosy_lab.java_smt.api.Model.ValueAssignment;
2123
import org.sosy_lab.java_smt.api.SolverException;
2224
import org.sosy_lab.java_smt.delegate.statistics.TimerPool.TimerWrapper;
2325

@@ -92,6 +94,11 @@ public Model getModel() throws SolverException {
9294
return new StatisticsModel(delegate.getModel(), stats);
9395
}
9496

97+
@Override
98+
public ImmutableList<ValueAssignment> getModelAssignments() throws SolverException {
99+
return delegate.getModelAssignments();
100+
}
101+
95102
@Override
96103
public List<BooleanFormula> getUnsatCore() {
97104
stats.unsatCore.getAndIncrement();

‎src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010

1111
import static com.google.common.base.Preconditions.checkNotNull;
1212

13+
import com.google.common.collect.ImmutableList;
1314
import com.google.common.collect.ImmutableMap;
1415
import java.util.Collection;
1516
import java.util.List;
@@ -19,6 +20,7 @@
1920
import org.sosy_lab.java_smt.api.BasicProverEnvironment;
2021
import org.sosy_lab.java_smt.api.BooleanFormula;
2122
import org.sosy_lab.java_smt.api.Model;
23+
import org.sosy_lab.java_smt.api.Model.ValueAssignment;
2224
import org.sosy_lab.java_smt.api.SolverContext;
2325
import org.sosy_lab.java_smt.api.SolverException;
2426

@@ -88,6 +90,11 @@ public Model getModel() throws SolverException {
8890
}
8991
}
9092

93+
@Override
94+
public ImmutableList<ValueAssignment> getModelAssignments() throws SolverException {
95+
return delegate.getModelAssignments();
96+
}
97+
9198
@Override
9299
public List<BooleanFormula> getUnsatCore() {
93100
synchronized (sync) {

‎src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@
2121
import org.sosy_lab.java_smt.api.BooleanFormula;
2222
import org.sosy_lab.java_smt.api.FormulaManager;
2323
import org.sosy_lab.java_smt.api.Model;
24+
import org.sosy_lab.java_smt.api.Model.ValueAssignment;
2425
import org.sosy_lab.java_smt.api.SolverContext;
2526
import org.sosy_lab.java_smt.api.SolverException;
2627

@@ -98,6 +99,11 @@ public Model getModel() throws SolverException {
9899
}
99100
}
100101

102+
@Override
103+
public ImmutableList<ValueAssignment> getModelAssignments() throws SolverException {
104+
return delegate.getModelAssignments();
105+
}
106+
101107
@Override
102108
public List<BooleanFormula> getUnsatCore() {
103109
return translate(delegate.getUnsatCore(), otherManager, manager);

‎src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java‎

Lines changed: 4 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,6 @@ public boolean terminate() {
4848
private final BitwuzlaFormulaManager manager;
4949

5050
private final BitwuzlaFormulaCreator creator;
51-
protected boolean wasLastSatCheckSat = false; // and stack is not changed
5251

5352
protected BitwuzlaTheoremProver(
5453
BitwuzlaFormulaManager pManager,
@@ -143,11 +142,8 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException {
143142
* @param assumptions A list of literals.
144143
*/
145144
@Override
146-
public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
145+
protected boolean isUnsatWithAssumptionsImpl(Collection<BooleanFormula> assumptions)
147146
throws SolverException, InterruptedException {
148-
Preconditions.checkState(!closed);
149-
wasLastSatCheckSat = false;
150-
151147
Collection<Term> newAssumptions = new LinkedHashSet<>();
152148
for (BooleanFormula formula : assumptions) {
153149
Term term = creator.extractInfo(formula);
@@ -170,8 +166,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
170166
*/
171167
@SuppressWarnings("resource")
172168
@Override
173-
public Model getModel() throws SolverException {
174-
Preconditions.checkState(!closed);
169+
protected Model getModelImpl() throws SolverException {
175170
Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP);
176171
checkGenerateModels();
177172
return new CachingModel(
@@ -196,9 +191,7 @@ private List<BooleanFormula> getUnsatCore0() {
196191
* returned <code>false</code>.
197192
*/
198193
@Override
199-
public List<BooleanFormula> getUnsatCore() {
200-
Preconditions.checkState(!closed);
201-
checkGenerateUnsatCores();
194+
protected List<BooleanFormula> getUnsatCoreImpl() {
202195
Preconditions.checkState(!wasLastSatCheckSat);
203196
return getUnsatCore0();
204197
}
@@ -212,12 +205,8 @@ public List<BooleanFormula> getUnsatCore() {
212205
* assumptions which is unsatisfiable with the original constraints otherwise.
213206
*/
214207
@Override
215-
public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
208+
protected Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
216209
Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
217-
Preconditions.checkNotNull(assumptions);
218-
Preconditions.checkState(!closed);
219-
checkGenerateUnsatCores(); // FIXME: JavaDoc say ProverOptions.GENERATE_UNSAT_CORE is not needed
220-
Preconditions.checkState(!wasLastSatCheckSat);
221210
boolean sat = !isUnsatWithAssumptions(assumptions);
222211
return sat ? Optional.empty() : Optional.of(getUnsatCore0());
223212
}

‎src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,6 @@ abstract class BoolectorAbstractProver<T> extends AbstractProverWithAllSat<T> {
3333
private final long btor;
3434
private final BoolectorFormulaManager manager;
3535
private final BoolectorFormulaCreator creator;
36-
protected boolean wasLastSatCheckSat = false; // and stack is not changed
3736
private final TerminationCallback terminationCallback;
3837
private final long terminationCallbackHelper;
3938

@@ -114,7 +113,7 @@ protected void pushImpl() throws InterruptedException {
114113
}
115114

116115
@Override
117-
public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
116+
protected boolean isUnsatWithAssumptionsImpl(Collection<BooleanFormula> pAssumptions)
118117
throws SolverException, InterruptedException {
119118
Preconditions.checkState(!closed);
120119
for (BooleanFormula assumption : pAssumptions) {
@@ -125,8 +124,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
125124

126125
@SuppressWarnings("resource")
127126
@Override
128-
public Model getModel() throws SolverException {
129-
Preconditions.checkState(!closed);
127+
protected Model getModelImpl() throws SolverException {
130128
Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP);
131129
checkGenerateModels();
132130
return new CachingModel(getEvaluatorWithoutChecks());
@@ -139,13 +137,13 @@ protected BoolectorModel getEvaluatorWithoutChecks() {
139137
}
140138

141139
@Override
142-
public List<BooleanFormula> getUnsatCore() {
140+
protected List<BooleanFormula> getUnsatCoreImpl() {
143141
throw new UnsupportedOperationException("Unsat core is not supported by Boolector.");
144142
}
145143

146144
@Override
147-
public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
148-
Collection<BooleanFormula> pAssumptions) throws SolverException, InterruptedException {
145+
protected Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
146+
Collection<BooleanFormula> pAssumptions) {
149147
throw new UnsupportedOperationException(
150148
"Unsat core with assumptions is not supported by Boolector.");
151149
}

0 commit comments

Comments
 (0)