Package org.sosy_lab.java_smt.api

Interface UserPropagator

All Known Implementing Classes:

AbstractUserPropagator, NQueensConstraintPropagator, NQueensEnumeratingPropagator

public interface UserPropagator

Allows user-defined propagators (~ theory solvers) to be implemented. It is advised to inherit from AbstractUserPropagator rather than implementing this interface directly.

A user propagator provides various callbacks that are invoked by the solver during the solving process. Within these callbacks, the user can react to and influence the solver by calling into the PropagatorBackend. For example, he can raise conflicts whenever the solver makes assignments inconsistent to the user-defined theory.

Method Summary

Modifier and Type	Method	Description
void	initializeWithBackend(PropagatorBackend backend)	This method is invoked after the user propagator is registered via BasicProverEnvironment.registerUserPropagator(UserPropagator).
void	onDecision(BooleanFormula expr, boolean value)	This callback is invoked if the solver decides to branch on a registered expression.
void	onFinalCheck()	This callback is invoked when the solver finds a complete satisfying assignment.
void	onKnownValue(BooleanFormula expr, boolean value)	This callback is invoked if the solver gets to know the value of a registered expression (registerExpression(org.sosy_lab.java_smt.api.BooleanFormula)).
void	onPop(int numPoppedLevels)	This callback is invoked when the solver backtracks.
void	onPush()	This callback is invoked whenever the solver creates a new decision level.
void	registerExpression(BooleanFormula theoryExpr)	Registers an expression to be observed by the UserPropagator.

Method Detail

onPush

void onPush()

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) or BasicProverEnvironment.pop().

onPop

void onPop(int numPoppedLevels)

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) or BasicProverEnvironment.pop().

Parameters:

numPoppedLevels - The number of levels to backtrack (~ number of pushes to backtrack).

onFinalCheck

void onFinalCheck()

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 via PropagatorBackend.propagateConflict(BooleanFormula[]).

Note: This callback is only invoked if the user propagator enabled it via PropagatorBackend.notifyOnFinalCheck().

onKnownValue

void onKnownValue(BooleanFormula expr,
                  boolean value)

This callback is invoked if the solver gets to know the value of a registered expression (registerExpression(org.sosy_lab.java_smt.api.BooleanFormula)). Within the callback, the user can raise conflicts via PropagatorBackend.propagateConflict(org.sosy_lab.java_smt.api.BooleanFormula[]), propagate consequences via PropagatorBackend.propagateConsequence(org.sosy_lab.java_smt.api.BooleanFormula[], org.sosy_lab.java_smt.api.BooleanFormula), or influence the solvers decision heuristics via PropagatorBackend.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().

Parameters:

expr - The expressions whose value is known.

value - The value of the expression.

onDecision

void onDecision(BooleanFormula expr,
                boolean value)

This callback is invoked if the solver decides to branch on a registered expression. (registerExpression(org.sosy_lab.java_smt.api.BooleanFormula)). Within the callback, the user can change the decision by calling PropagatorBackend.propagateNextDecision(org.sosy_lab.java_smt.api.BooleanFormula, java.util.Optional<java.lang.Boolean>).

Note: This callback is only invoked if the user propagator enabled it via PropagatorBackend.notifyOnDecision().

Parameters:

expr - The expressions whose value gets decided (usually a literal).

value - The decision value.

initializeWithBackend

void initializeWithBackend(PropagatorBackend backend)

This method is invoked after the user propagator is registered via BasicProverEnvironment.registerUserPropagator(UserPropagator). The user can enable notifications by accessing the provided PropagatorBackend.

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.

registerExpression

void registerExpression(BooleanFormula theoryExpr)

Registers an expression to be observed by the UserPropagator. Solver actions related to the expression are reported:

• The callback onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean) gets invoked if the value of a registered expression becomes known (if notification was enabled via PropagatorBackend.notifyOnKnownValue()).
• The callback onDecision(org.sosy_lab.java_smt.api.BooleanFormula, boolean) gets invoked right before the solver decides on the value of a registered expression (if notification was enabled via PropagatorBackend.notifyOnDecision()).

Parameters:

theoryExpr - The expression to observe.