Class NQueensConstraintPropagator
- java.lang.Object
-
- org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator
-
- org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator
-
- org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensConstraintPropagator
-
- All Implemented Interfaces:
UserPropagator
public class NQueensConstraintPropagator extends NQueensEnumeratingPropagator
In addition to the enumeration done byNQueensEnumeratingPropagator
, this propagator also enforces the queen placement constraints without explicit encoding.
-
-
Field Summary
-
Fields inherited from class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator
currentModel, fixedCount, fixedVariables, modelSet
-
-
Constructor Summary
Constructors Constructor Description NQueensConstraintPropagator(BooleanFormula[][] symbols)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description 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)
).-
Methods inherited from class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator
getNumOfSolutions, initializeWithBackend, onFinalCheck, onPop, onPush
-
Methods inherited from class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator
getBackend, onDecision, registerExpression
-
-
-
-
Constructor Detail
-
NQueensConstraintPropagator
public NQueensConstraintPropagator(BooleanFormula[][] symbols)
-
-
Method Detail
-
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 classNQueensEnumeratingPropagator
- Parameters:
var
- The expressions whose value is known.value
- The value of the expression.
-
-