Class GhostQSolver

    • Field Summary

      Fields 
      Modifier and Type Field Description
      private java.lang.String binaryLocation
      String representation of the GhostQ binary path.
      • Fields inherited from class net.sf.tweety.logics.qbf.reasoner.QbfSolver

        bash
    • Constructor Summary

      Constructors 
      Constructor Description
      GhostQSolver​(java.lang.String binaryLocation)
      Constructs a new instance pointing to a specific GhostQSolver
      GhostQSolver​(java.lang.String binaryLocation, Shell bash)
      Constructs a new instance pointing to a specific GhostQSolver.
    • Method Summary

      Modifier and Type Method Description
      private boolean evaluate​(java.io.File file, java.io.File file2)
      Invokes GhostQ with the given input file.
      boolean isSatisfiable​(java.util.Collection<PlFormula> kb)
      Checks whether the given set of formulas is satisfiable.
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Field Detail

      • binaryLocation

        private java.lang.String binaryLocation
        String representation of the GhostQ binary path. Temporary files are stored in this directory.
    • Constructor Detail

      • GhostQSolver

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

        public GhostQSolver​(java.lang.String binaryLocation)
        Constructs a new instance pointing to a specific GhostQSolver
        Parameters:
        binaryLocation - of the GhostQ executable on the hard drive
    • Method Detail

      • evaluate

        private boolean evaluate​(java.io.File file,
                                 java.io.File file2)
                          throws java.lang.Exception
        Invokes GhostQ with the given input file.
        Parameters:
        file - input file for GhostQ
        file2 -
        Returns:
        true if the result is SAT, false if the result is UNSAT
        Throws:
        java.lang.Exception - if the bash command fails or if GhostQ produces no interpretable output
      • isSatisfiable

        public boolean isSatisfiable​(java.util.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.