Package org.sosy_lab.java_smt.api

Interface PropagatorBackend

public interface PropagatorBackend

The PropagatorBackend class is used by UserPropagator to implement custom user propagators. It contains functions to interact with the SAT/SMT core during solving, for example, it provides the ability to propagate conflicts and to influence the decision-making.

Method Summary

Modifier and Type	Method	Description
void	notifyOnDecision()	Enables tracking of decisions made for the associated UserPropagator via UserPropagator.onDecision(BooleanFormula, boolean).
void	notifyOnFinalCheck()	Enables the final callback UserPropagator.onFinalCheck() that is invoked when the solver finds a full satisfying assignment.
void	notifyOnKnownValue()	Enables tracking of expression values for the associated UserPropagator via UserPropagator.onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean).
void	propagateConflict(BooleanFormula[] conflictExpressions)	Raises a conflict caused by a set of conflicting assignments.
void	propagateConsequence(BooleanFormula[] assignedExpressions, BooleanFormula consequence)	Propagates a consequence implied by a set of assigned expressions.
boolean	propagateNextDecision(BooleanFormula expr, Optional<Boolean> value)	Propagates a decision to be made by the solver.
void	registerExpression(BooleanFormula theoryExpr)	Registers an expression to be observed by a UserPropagator.

Method Detail

registerExpression

void registerExpression(BooleanFormula theoryExpr)

Registers an expression to be observed by a UserPropagator. See UserPropagator.onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean) and UserPropagator.onDecision(org.sosy_lab.java_smt.api.BooleanFormula, boolean) for more information.

Parameters:

theoryExpr - The expression to observe.

propagateConflict

void propagateConflict(BooleanFormula[] conflictExpressions)

Raises a conflict caused by a set of conflicting assignments. Shall only be called from within a callback by UserPropagator such as UserPropagator.onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean) and UserPropagator.onFinalCheck().

Effectively causes the solver to learn the implication "conflictExpressions => false"

Parameters:

conflictExpressions - A set of inconsistent assignments.

propagateConsequence

void propagateConsequence(BooleanFormula[] assignedExpressions,
                          BooleanFormula consequence)

Propagates a consequence implied by a set of assigned expressions. Shall only be called from within a callback by UserPropagator such as UserPropagator.onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean) and UserPropagator.onFinalCheck().

Effectively causes the solver to learn the implication "/\ assignedExpressions => consequence" It is possible to have an empty set of assignedExpressions to generate a theory lemma.

Parameters:

assignedExpressions - A set of assigned expressions.

consequence - The consequence implied by the assigned expressions.

propagateNextDecision

boolean propagateNextDecision(BooleanFormula expr,
                              Optional<Boolean> value)

Propagates a decision to be made by the solver. If called during UserPropagator.onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean), will set the next decision to be made. If called during UserPropagator.onDecision(org.sosy_lab.java_smt.api.BooleanFormula, boolean), will overwrite the current decision to be made.

Parameters:

expr - The expression to assign to next.

value - The value to be assigned. If not given, the solver will decide.

Returns:

False, if the value of expr is already assigned. True, otherwise. Note that the value of expr may already be decided before being reported via UserPropagator.onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean).

notifyOnKnownValue

void notifyOnKnownValue()

Enables tracking of expression values for the associated UserPropagator via UserPropagator.onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean).

This function is typically called from UserPropagator.initializeWithBackend(org.sosy_lab.java_smt.api.PropagatorBackend) if the theory solver needs to listen to the value of expressions registered by registerExpression(org.sosy_lab.java_smt.api.BooleanFormula).

notifyOnDecision

void notifyOnDecision()

Enables tracking of decisions made for the associated UserPropagator via UserPropagator.onDecision(BooleanFormula, boolean).

This function is typically called from UserPropagator.initializeWithBackend(org.sosy_lab.java_smt.api.PropagatorBackend) if the theory solver needs to listen to and/or modify the decisions made by the solver on expressions registered by registerExpression(org.sosy_lab.java_smt.api.BooleanFormula).

notifyOnFinalCheck

void notifyOnFinalCheck()

Enables the final callback UserPropagator.onFinalCheck() that is invoked when the solver finds a full satisfying assignment.

This function is typically called from UserPropagator.initializeWithBackend(org.sosy_lab.java_smt.api.PropagatorBackend) if the theory solver needs to perform final consistency checks.