Package org.tweetyproject.lp.asp.reasoner

Class DLVSolver

java.lang.Object
org.tweetyproject.lp.asp.reasoner.ASPSolver
org.tweetyproject.lp.asp.reasoner.DLVSolver
All Implemented Interfaces:
ModelProvider<ASPRule,Program,AnswerSet>, QualitativeReasoner<Program,ASPLiteral>, Reasoner<Boolean,Program,ASPLiteral>
public class DLVSolver extends ASPSolver
Wrapper class for the DLV answer set solver command line utility.
Author:
Thomas Vengels, Tim Janus, Anna Gessler

  • Constructor Details

    • DLVSolver

      public DLVSolver(String pathToDLV)
      Constructs a new instance pointing to a specific DLV solver.
      Parameters:
      pathToDLV - binary location of DLV on the hard drive. The given location has to contain a binary called "dlv". Do not include the binary itself in the path.

    • DLVSolver

      public DLVSolver(String pathToDLV, Shell bash)
      Constructs a new instance pointing to a specific DLV solver.
      Parameters:
      pathToDLV - binary location of DLV on the hard drive. The given location has to contain a binary called "dlv". Do not include the binary itself in the path.
      bash - shell to run commands

    • DLVSolver

      public DLVSolver(String pathToDLV, int maxNOfModels, int integerMaximum)
      Constructs a new instance pointing to a specific DLV solver.
      Parameters:
      pathToDLV - binary location of Clingo on the hard drive. The given location has to contain a binary called "clingo". Do not include the binary itself in the path.
      maxNOfModels - the maximum number of models that DLV will compute.
      integerMaximum - the integer maximum ("-N" parameter) that DLV will use

  • Method Details

    • getModels

      public Collection<AnswerSet> getModels(Program p, int maxInt)
      Returns a characterizing model (answer set) of the given belief base using the given upper integer limit.
      Overrides:
      getModels in class ASPSolver
      Parameters:
      p - a program
      maxInt - the max number of models to be returned
      Returns:
      AnswerSet

    • getModel

      public AnswerSet getModel(Program p, int maxInt)
      Returns a characterizing model (answer set) of the given belief base using the given upper integer limit.
      Overrides:
      getModel in class ASPSolver
      Parameters:
      p - a program
      maxInt - the max number of models to be returned
      Returns:
      AnswerSet

    • getModels

      public List<AnswerSet> getModels(Program p)
      Description copied from interface: ModelProvider
      Returns a characterizing model of the given belief base
      Specified by:
      getModels in interface ModelProvider<ASPRule,Program,AnswerSet>
      Specified by:
      getModels in class ASPSolver
      Parameters:
      p - some belief base
      Returns:
      the (selected) models of the belief base

    • getModels

      public List<AnswerSet> getModels(String p)
      Description copied from class: ASPSolver
      Returns a characterizing model (answer set) of the given belief base.
      Specified by:
      getModels in class ASPSolver
      Parameters:
      p - containing belief base
      Returns:
      AnswerSet

    • getModels

      public List<AnswerSet> getModels(File file)
      Description copied from class: ASPSolver
      Returns a characterizing model (answer set) of the given belief base.
      Specified by:
      getModels in class ASPSolver
      Parameters:
      file - containing belief base
      Returns:
      AnswerSet

    • getModel

      public AnswerSet getModel(Program p)
      Description copied from interface: ModelProvider
      Returns a single (dedicated) model of the given belief base. If the implemented method allows for more than one dedicated model, the selection may be non-deterministic.
      Parameters:
      p - some belief base
      Returns:
      a selected model of the belief base.

    • setOptions

      public void setOptions(String options)
      Set additional command line options for DLV.
      Parameters:
      options - a string of options

    • setPathToDLV

      public void setPathToDLV(String pathToDLV)
      Sets the location of the DLV solver on the hard drive.
      Parameters:
      pathToDLV - path to DLV

    • query

      public Boolean query(Program beliefbase, ASPLiteral formula)
      Description copied from interface: Reasoner
      Queries the given belief base for the given formula.
      Specified by:
      query in interface QualitativeReasoner<Program,ASPLiteral>
      Specified by:
      query in interface Reasoner<Boolean,Program,ASPLiteral>
      Specified by:
      query in class ASPSolver
      Parameters:
      beliefbase - a belief base
      formula - a formula
      Returns:
      the answer to the query

    • query

      public Boolean query(Program beliefbase, ASPLiteral formula, InferenceMode inferenceMode)

    • isInstalled

      public boolean isInstalled()
      Returns:
      if the solver is installed