Interface Theory

public interface Theory

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    static final int
    DEFAULT_PRIORITY
    The default priority for theory propagators.
    static final int
    DIVERGING_PRIORITY
    The recommended priority for theory propagators that might diverge (i.e., execute continuously without reaching fixed point) on unsatisfiable problems.

  • Method Summary

    Modifier and Type
    Method
    Description
    TheorySupport
    checkSupport(TheoryRule theoryRule)
     
    void
    createPropagator(ModelStoreBuilder storeBuilder, Collection<TheoryRule> collectedRules)
     
    default int
    getPriority()
    Gets the priority that determines where in the sequence of propagator should this theory run.

  • Field Details

    • DEFAULT_PRIORITY

      static final int DEFAULT_PRIORITY
      The default priority for theory propagators.
      See Also:

    • DIVERGING_PRIORITY

      static final int DIVERGING_PRIORITY
      The recommended priority for theory propagators that might diverge (i.e., execute continuously without reaching fixed point) on unsatisfiable problems.

      Propagators with this priority will run late enough in the sequence of propagators so that theory propagators that can detect global unsatisfiability have already finished and determined that the numerical problem is satisfiable.

      See Also:

  • Method Details

    • checkSupport

      TheorySupport checkSupport(TheoryRule theoryRule)

    • createPropagator

      void createPropagator(ModelStoreBuilder storeBuilder, Collection<TheoryRule> collectedRules)

    • getPriority

      default int getPriority()
      Gets the priority that determines where in the sequence of propagator should this theory run.

      Higher values denote a request to appear earlier in the sequence of propagators.

      Returns:
      The priority. The default priority is DEFAULT_PRIORITY.