Package io.github.cvc5

Class AbstractPlugin

java.lang.Object
io.github.cvc5.AbstractPlugin
public abstract class AbstractPlugin extends Object
A cvc5 plugin abstract class.

  • Field Details

    • termManager

      protected final TermManager termManager
      The associated term manager.

  • Constructor Details

    • AbstractPlugin

      public AbstractPlugin(TermManager tm)
      Create plugin instance.
      Parameters:
      tm - The associated term manager.

  • Method Details

    • getTermManager

      public TermManager getTermManager()
      Get the associated term manager instance
      Returns:
      The term manager.

    • check

      public Term[] check()
      Call to check, return vector of lemmas to add to the SAT solver. This method is called periodically, roughly at every SAT decision.
      Returns:
      The vector of lemmas to add to the SAT solver.

    • notifySatClause

      public void notifySatClause(Term cl)
      Notify SAT clause, called when cl is a clause learned by the SAT solver.
      Parameters:
      cl - The learned clause.

    • notifyTheoryLemma

      public void notifyTheoryLemma(Term lem)
      Notify theory lemma, called when lem is a theory lemma sent by a theory solver.
      Parameters:
      lem - The theory lemma.

    • getName

      public abstract String getName()
      Get the name of the plugin (for debugging).
      Returns:
      The name of the plugin.