Package org.sosy_lab.java_smt.api
Interface BasicProverEnvironment.AllSatCallback<R>
-
- Type Parameters:
R
- The result type of the callback, passed through byBasicProverEnvironment.allSat(org.sosy_lab.java_smt.api.BasicProverEnvironment.AllSatCallback<R>, java.util.List<org.sosy_lab.java_smt.api.BooleanFormula>)
.
- Enclosing interface:
- BasicProverEnvironment<T>
public static interface BasicProverEnvironment.AllSatCallback<R>
-
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method Description void
apply(List<BooleanFormula> model)
Callback for each possible satisfying assignment to givenimportant
predicates.R
getResult()
Returning the result generated after all theapply(java.util.List<org.sosy_lab.java_smt.api.BooleanFormula>)
calls went through.
-
-
-
Method Detail
-
apply
void apply(List<BooleanFormula> model)
Callback for each possible satisfying assignment to givenimportant
predicates. If the predicate is assignedtrue
in the model, it is returned as-is in the list, and otherwise it is negated.There is no guarantee that the list of model values corresponds to the list in
BasicProverEnvironment.allSat(org.sosy_lab.java_smt.api.BasicProverEnvironment.AllSatCallback<R>, java.util.List<org.sosy_lab.java_smt.api.BooleanFormula>)
. We can reorder the variables or leave out values with a freely chosen value.
-
getResult
R getResult() throws InterruptedException
Returning the result generated after all theapply(java.util.List<org.sosy_lab.java_smt.api.BooleanFormula>)
calls went through.- Throws:
InterruptedException
-
-