GhostQSolver

java.lang.Object

org.tweetyproject.logics.qbf.reasoner.QbfSolver

org.tweetyproject.logics.qbf.reasoner.GhostQSolver

All Implemented Interfaces:: BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>

public class GhostQSolver extends QbfSolver

A wrapper for the GhostQ (https://www.wklieber.com/ghostq/) solver.
Tested with the GhostQ 2017 version: https://www.wklieber.com/ghostq/2017.html/

Author:: Anna Gessler

Constructor Summary

Constructors

Constructor

Description

GhostQSolver(String binaryLocation)

Constructs a new instance pointing to a specific GhostQSolver

GhostQSolver(String binaryLocation, Shell bash)

Constructs a new instance pointing to a specific GhostQSolver.
Method Summary

Modifier and Type

Method

Description

boolean

isSatisfiable(Collection<PlFormula> kb)

Checks whether the given set of formulas is satisfiable.

Methods inherited from class org.tweetyproject.logics.qbf.reasoner.QbfSolver
isConsistent, isConsistent, isConsistent

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details
- GhostQSolver
  
  public GhostQSolver(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(String binaryLocation)
  
  Constructs a new instance pointing to a specific GhostQSolver
  
  Parameters:
  
  binaryLocation - of the GhostQ 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.