Class CadetSolver

java.lang.Object
org.tweetyproject.logics.qbf.reasoner.QbfSolver
org.tweetyproject.logics.qbf.reasoner.CadetSolver
All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>

public class CadetSolver extends QbfSolver
A wrapper for the Cadet (https://markusrabe.github.io/cadet/) solver. Tested with version 2.5.
Author:
Anna Gessler
  • Constructor Details

    • CadetSolver

      public CadetSolver(String binaryLocation, Shell bash)
      Constructs a new instance pointing to a specific CadetSolver.
      Parameters:
      binaryLocation - of the GhostQ executable on the hard drive
      bash - shell to run commands
    • CadetSolver

      public CadetSolver(String binaryLocation)
      Constructs a new instance pointing to a specific CadetSolver
      Parameters:
      binaryLocation - of the CadetSolver executable on the hard drive
  • Method Details

    • isSatisfiable

      public boolean isSatisfiable(Collection<PlFormula> kb)
      Description copied from class: QbfSolver
      Checks whether the given set of formulas is satisfiable.
      Specified by:
      isSatisfiable in class QbfSolver
      Parameters:
      kb - a set of formulas.
      Returns:
      "true" if the set is consistent.
    • isInstalled

      public boolean isInstalled()
      Specified by:
      isInstalled in class QbfSolver