Class NQueensEnumeratingPropagator
- java.lang.Object
-
- org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator
-
- org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator
-
- All Implemented Interfaces:
UserPropagator
- Direct Known Subclasses:
NQueensConstraintPropagator
public class NQueensEnumeratingPropagator extends AbstractUserPropagator
This propagator enumerates the solutions of the NQueens problem by raising a conflict whenever the solver finds a model.
-
-
Field Summary
Fields Modifier and Type Field Description protected Map<BooleanFormula,Boolean>
currentModel
protected Deque<Integer>
fixedCount
protected Deque<BooleanFormula>
fixedVariables
protected Set<Map<BooleanFormula,Integer>>
modelSet
-
Constructor Summary
Constructors Constructor Description NQueensEnumeratingPropagator()
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description int
getNumOfSolutions()
void
initializeWithBackend(PropagatorBackend backend)
This method is invoked after the user propagator is registered viaBasicProverEnvironment.registerUserPropagator(UserPropagator)
.void
onFinalCheck()
This callback is invoked when the solver finds a complete satisfying assignment.void
onKnownValue(BooleanFormula var, boolean value)
This callback is invoked if the solver gets to know the value of a registered expression (UserPropagator.registerExpression(org.sosy_lab.java_smt.api.BooleanFormula)
).void
onPop(int numPoppedLevel)
This callback is invoked when the solver backtracks.void
onPush()
This callback is invoked whenever the solver creates a new decision level.-
Methods inherited from class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator
getBackend, onDecision, registerExpression
-
-
-
-
Field Detail
-
fixedVariables
protected final Deque<BooleanFormula> fixedVariables
-
currentModel
protected final Map<BooleanFormula,Boolean> currentModel
-
modelSet
protected final Set<Map<BooleanFormula,Integer>> modelSet
-
-
Method Detail
-
getNumOfSolutions
public int getNumOfSolutions()
-
onPush
public void onPush()
Description copied from interface:UserPropagator
This callback is invoked whenever the solver creates a new decision level. A user propagator should maintain backtracking points on each push to enable later backtracking.The onPush or onPop operation refers to internal state of the SMT/SAT solver while running a SAT check. This does not relate to Prover operations in the SMT-based API, such as
BasicProverEnvironment.push(org.sosy_lab.java_smt.api.BooleanFormula)
orBasicProverEnvironment.pop()
.- Specified by:
onPush
in interfaceUserPropagator
- Overrides:
onPush
in classAbstractUserPropagator
-
onPop
public void onPop(int numPoppedLevel)
Description copied from interface:UserPropagator
This callback is invoked when the solver backtracks. The solver can backtrack multiple levels simultaneously.The onPush or onPop operation refers to internal state of the SMT/SAT solver while running a SAT check. This does not relate to Prover operations in the SMT-based API, such as
BasicProverEnvironment.push(org.sosy_lab.java_smt.api.BooleanFormula)
orBasicProverEnvironment.pop()
.- Specified by:
onPop
in interfaceUserPropagator
- Overrides:
onPop
in classAbstractUserPropagator
- Parameters:
numPoppedLevel
- The number of levels to backtrack (~ number of pushes to backtrack).
-
onFinalCheck
public void onFinalCheck()
Description copied from interface:UserPropagator
This callback is invoked when the solver finds a complete satisfying assignment. The user can check the found model for consistency and potentially raise conflicts viaPropagatorBackend.propagateConflict(BooleanFormula[])
.Note: This callback is only invoked if the user propagator enabled it via
PropagatorBackend.notifyOnFinalCheck()
.- Specified by:
onFinalCheck
in interfaceUserPropagator
- Overrides:
onFinalCheck
in classAbstractUserPropagator
-
onKnownValue
public void onKnownValue(BooleanFormula var, boolean value)
Description copied from interface:UserPropagator
This callback is invoked if the solver gets to know the value of a registered expression (UserPropagator.registerExpression(org.sosy_lab.java_smt.api.BooleanFormula)
). Within the callback, the user can raise conflicts viaPropagatorBackend.propagateConflict(org.sosy_lab.java_smt.api.BooleanFormula[])
, propagate consequences viaPropagatorBackend.propagateConsequence(org.sosy_lab.java_smt.api.BooleanFormula[], org.sosy_lab.java_smt.api.BooleanFormula)
, or influence the solvers decision heuristics viaPropagatorBackend.propagateNextDecision(org.sosy_lab.java_smt.api.BooleanFormula, java.util.Optional<java.lang.Boolean>)
.The reported value is only known on the current and later push levels, but will get invalidated when backtracking.
Note: This callback is only invoked if the user propagator enabled it via
PropagatorBackend.notifyOnKnownValue()
.- Specified by:
onKnownValue
in interfaceUserPropagator
- Overrides:
onKnownValue
in classAbstractUserPropagator
- Parameters:
var
- The expressions whose value is known.value
- The value of the expression.
-
initializeWithBackend
public void initializeWithBackend(PropagatorBackend backend)
Description copied from interface:UserPropagator
This method is invoked after the user propagator is registered viaBasicProverEnvironment.registerUserPropagator(UserPropagator)
. The user can enable notifications by accessing the providedPropagatorBackend
.Warning: During its lifetime, a user propagator shall only be registered once via
BasicProverEnvironment.registerUserPropagator(UserPropagator)
for otherwise unexpected errors can occur. Implementations are advised to throw exceptions if this method is called multiple times.- Specified by:
initializeWithBackend
in interfaceUserPropagator
- Overrides:
initializeWithBackend
in classAbstractUserPropagator
-
-